% !Mode:: "TeX:UTF-8"
%\documentclass[14pt, twoside]{extreport}
\documentclass[14pt, twoside]{extarticle}
\usepackage{cmap}

%\usepackage{fix-cm}
\usepackage[utf8]{inputenx}
\usepackage[russian]{babel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%\usepackage{pscyr}
%\usepackage[T1]{fontenc} %cm-super
%\usepackage{type1cm}
\usepackage{indentfirst}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{dsfont}
\usepackage{xspace}
\usepackage[numbers,compress,sort]{natbib}
\usepackage{clrscode}

\pagestyle{headings}

\textheight 23cm % 29.7-2-2
\textwidth 16cm % 21-2.5-1.5
\hoffset 0.46cm %2.5-2.54 слева 3 см
\voffset -0.54cm %2-2.54 сверху 2 см
\oddsidemargin 0cm \evensidemargin 0cm  \headheight 0cm \headsep 1.5cm \topmargin 0cm

\usepackage{ccaption} % заменяем для рисунков ':' после номера рисунка на другой символ
\captiondelim{. } % разделитель точка и пробел

\usepackage{vaucanson-g}

\usepackage{ifpdf}

\ifpdf
% we are running pdflatex, so convert .eps files to .pdf
% run pdflatex with --shell-escape and thesis.aux
\usepackage[pdftex]{graphicx}
\usepackage{epstopdf}
\else
% we are running LaTeX, not pdflatex
\usepackage{graphicx}
\fi

% Подправим команду \appendix : нумерация русскими буквами,
% а не латинскими.
\makeatletter
\renewcommand\appendix{\par
%  \setcounter{chapter}{0}%
  \setcounter{section}{0}%
  \def\@chapapp{\appendixname}%
  \def\thechapter{\@Asbuk\c@chapter}}
\makeatother

% "русифицируем" окружение enumerate:
\makeatletter
\def\labelenumi{\theenumi)}      % чтобы после номера шла скобка;
\def\theenumii{\@asbuk\c@enumii}   % чтобы на втором уровне шли русские,
\def\labelenumii{\theenumii)}    % а не латинские буквы
\def\p@enumii{\theenumi}         % а это для \ref
\def\labelenumiii{{\bf--}}       % а на третьем уровне пусть будут лишь тире,
\let\theenumiii\relax            % и отдельных ссылок на него не будет
\def\p@enumiii{\theenumi\theenumii}
\makeatother

\usepackage{rsl}

\usepackage{listingsutf8}
\lstloadlanguages{RSL}
\lstset{numbers=left, language=RSL, extendedchars=true, numberstyle=\tiny, inputencoding=utf8%,
%commentstyle=\itshape, stringstyle=\bfseries
}

\author{Евгений Корныхин}
\title{\huge{\textbf{\textsc{Семинарские занятия по формальной функциональной спецификации программ}}}}
%\date{Москва --- 2010}

%\newcounter{problem_type}[chapter]
%\newcounter{zadacha}[problem_type]
%\newcommand{\z}{\vspace{0.5cm}\par\addtocounter{zadacha}{1}%
%\textit{\arabic{chapter}.\arabic{problem_type}.\arabic{zadacha}}~~  }

\newcounter{problem_type}[section]
\newcounter{zadacha}[problem_type]
\newcommand{\z}{\vspace{0.5cm}\par\addtocounter{zadacha}{1}%
\textit{\arabic{section}.\arabic{problem_type}.\arabic{zadacha}}~~  }

\newcommand{\head}[1]{\vspace{1cm}\subsubsection*{#1}}
\newcommand{\zhead}[1]{\head{#1} \refstepcounter{problem_type}}


\begin{document}

\maketitle

\tableofcontents

\input{intro}


%%%%%%%%%% Общая структура %%%%%%%%%%%
%%  0. "Введение". (см. igoogle) Создание формальной модели поведения системы как способ уточнения требований
%%  1. "Основные определения" (спецификация, модель, полнота, тотальность, непротиворечивость, явность).
%%      Нулевая задачка экзамена. Детерминированные функции, недетерминированные функции на примерах чисел.
%%      Первая задачка экзамена в том случае, когда всё состояние скрыто (т.е. про состояние пока что не думаем).
%%  2. "Языки спецификации". Сначала RSL (множества, списки, отображения). Потом ACSL (модель памяти, функции с указателями)
%%  3. "Модельные спецификации". Кроме самих данных, специфицируем состояние системы (модель состояния, инварианты).
%%      Первая задачка экзамена в полном объеме. Выделение ветвей функциональности при записи постусловий.
%%      Согласованность модельных спецификаций (инвариант не пуст после каждой функции, нет вызовов функций вне их предусловий)
%%  4. "Алгебраические спецификации". Понятие алгебраической спецификации (новая вторая задачка экзамена).
%%      Согласованность алгебраических спецификаций (бывшая вторая задачка экзамена).
%%  5. "Автоматные спецификации". Тут про третью задачку экзамена.
%%  6. ......... может быть сюда включить формальную верификацию...........

\pagebreak
\section{RSL для императивного программирования}

\input{prog/about}

\subsection*{Задачи}

\input{prog/problems}


\pagebreak
\section{Основные понятия}

\subsection{Спецификация функций}

Функциональная спецификация программы --- это набор синтаксических и семантических свойств функций, составляющих программу. Под <<функцией>> понимается некий код, текст на языке программирования (например, <<функция на языке Си>>). Синтаксические свойства функции --- это свойства сигнатуры функции (ее имя, количество и типы параметров). Синтаксические свойства выражаются в формальной спецификации указанием сигнатуры функции. Семантические свойства функции --- это свойства отображения входных данных на выходные, которое осуществляет функция. Семантические свойства задаются при помощи предикатов над значениями аргументов функции и значения функции при этих аргументах. Примеры семантических свойств функции (назовем ее $f(x)$, $x: \Int$, $f(x) : \Int$):

\begin{itemize}
  \item $f(0) = 0$ (утверждается значение функции при заданном значении ее аргументов);
  \item $\All x: \Int ~\SuchAs~ f(x) = -f(-x)$ (нечетность функции);
  \item $\Exists x: \Int ~\SuchAs~ f(x) \equiv \Chaos$ (функция на каком-то значении аргумента зацикливается);
  \item $f(x) = x + 1$, если $x = 0, 1, 2, .., 10$ (частичное задание функции);
  \item $f(x) = x + 1$, если $x = 0, 1, 2, ..., 10$, $f(x) = 0$, иначе (полное задание функции);
  \item у функции $f$ 1 аргумент (синтаксическое свойство функции);
  \item $f(0)$ может равняться 0 или 1 (это свойство можно трактовать двояко - либо функция $f(x)$ ведет себя \emph{недетерминированно} при $x = 0$ и может вернуть число 0 или число 1 (т.е. при работе программы с такой функцией могут возникнуть оба значения), либо функция $f(x)$ ведет себя детерминированно при $x = 0$ и $f(0)$ равняется одному из чисел 0 или 1 (при работе программы с такой функцией может возникнуть только одно из чисел)).
\end{itemize}

Для записи семантических свойств функций язык RSL предлагает пользоваться \emph{аксиомами}. Например, свойство $f(0) = 0$ будет записано следующим образом:

\begin{lstlisting}
value f: Int -~-> Int
axiom f(0) is 0
\end{lstlisting}

Свойство нечетности функции:
\begin{lstlisting}
value f: Int -~-> Int
axiom all x: Int :- f(x) is -f(-x)
\end{lstlisting}

Частичное определение функции можно дать следующим образом:
\begin{lstlisting}
value f: Int -~-> Int
axiom all x: Int :- x >= 0 /\ x <= 10 => f(x) is x+1
\end{lstlisting}

Но нагляднее будет воспользоваться \emph{\textbf{pre}-выражением}, ограничивающим область значений подкванторных переменных:
\begin{lstlisting}
value f: Int -~-> Int
axiom all x: Int :-
        f(x) is x + 1 pre x >= 0 /\ x <= 10
\end{lstlisting}

Полное определение можно дать с использованием одной аксиомы:
\begin{lstlisting}
value f: Int -~-> Int
axiom all x: Int :-
    f(x) is (if x >= 0 /\ x <= 10 then x+1 else 0 end)
\end{lstlisting}

или так:

\begin{lstlisting}
value f: Int -~-> Int
axiom all x: Int :-
    (x >= 0 /\ x <= 10 => f(x) is x + 1) /\
    ((x < 0 \/ x > 10) => f(x) is 0)
\end{lstlisting}

или с использованием двух аксиом:
\begin{lstlisting}
value f: Int -~-> Int
axiom
all x: Int :- f(x) is x + 1  pre x >= 0 /\ x <= 10,
all x: Int :- f(x) is 0  pre x < 0 \/ x > 10
\end{lstlisting}

можно воспользоваться конструкцией forall для сокращения количества кванторов всеобщности:
\begin{lstlisting}
value f: Int -~-> Int
axiom forall x: Int :-
    f(x) is x + 1  pre x >= 0 /\ x <= 10,
    f(x) is 0  pre x < 0 \/ x > 10
\end{lstlisting}

\head{Тотальная спецификация функции}

Если рассматривать однопроцессные однопотоковые невзаимодействующие с окружением программы, которые должны результативно завершаться (и только тогда такие программы имеют смысл), то про функции в программах можно говорить следующее:
\begin{itemize}
  \item на некоторых данных функция завершается;
  \item на некоторых данных функция завершается и ее результат детерминирован (т.е. будет точно таким же, если вызвать функцию с теми же аргументами и значениями глобальных переменных);
  \item на некоторых данных функция завершается и ее результат недетерминирован;
  \item на некоторых данных функция зацикливается (программа <<повисла>>);
  \item во время работы функция пытается выполнить недопустимую операцию (программа <<упала>>).
\end{itemize}

Для работы программы важно, чтобы ее функции не зацикливались и не <<падали>> как минимум на некотором <<нужном>> множестве входных данных (в противном случае этой функцией нельзя будет пользоваться).

Будем называть функцию \emph{тотальной}, если эта функция удовлетворяет следующим свойствам:
\begin{enumerate}
  \item она результативно завершима (т.е. не зацикливается и не падает ни при каком значении аргументов и глобальных переменных);
  \item результат функции детерминирован (если функция вызывается в разное время с теми же аргументами и в том же состоянии глобальных переменных, то она возвращает одинаковые значения и одинаковым образом изменяет глобальные переменные).
%  \item она всюду определена (функция возвращает какое-либо значение на каждом значении аргументов и глобальных переменных, согласно их типам);
\end{enumerate}

Спецификация может содержать требование функции быть тотальной. В этом случае в сигнатуре этой функции вместо стрелки $\NonDetermFn$ ставится стрелка $\Fn$. Однако спецификация может не содержать требования функции быть тотальной, но в коде реализации эта функция в действительности будет тотальной. Иначе говоря, \textit{стрелка $\NonDetermFn$ в сигнатуре не означает, что функция не является тотальной}. Стрелка $\NonDetermFn$ означает, что функция может быть какой угодно, как тотальной, так и нетотальной.

\head{Полное определение функции. Случай недоспецификации.}

Набор синтаксических и семантических свойств будем называть \emph{определением} функции, если семантические свойства дают возможность однозначно судить о значениях функции при всех входных данных, допустимых сигнатурой функции.

Спецификацию функции будем называть \emph{полной}, если она позволяет сделать вывод о значении функции при \textbf{каждом} значении ее аргументов и глобальных переменных. Остальные спецификации будем называть \emph{неполными}, или \emph{частичными}. При частичном задании удобно использовать \textbf{pre}-выражения (примеры были даны выше).

Пример полной спецификации:
\begin{lstlisting}
value f: Int >< Int -> Int
axiom forall x, y: Int :-
    f(x, y) is x + y pre x > y,
    f(x, y) is x - y pre x <= y
\end{lstlisting}
При каждом значении пары (x, y) в этой спецификации задано значение функции f. Тем самым эта спецификация функции f является полной.

Пример неполной спецификации:
\begin{lstlisting}
value f: Int >< Int -> Int
axiom forall x, y: Int :-
    f(x, y) is x + y pre x > y
\end{lstlisting}
Из этой спецификации можно сделать вывод о значении функции f на тех парах (x, y), где x > y, но нельзя сделать вывод  о значениях функции f на остальных парах. Тем самым, эта спецификация функции f является неполной. Эту спецификацию можно \emph{доопределить} до полной спецификации бесконечным числом способов (не нарушая требования тотальности функции f). Спецификацию, в которой есть неполная спецификаций какой-либо функции (или глобальной переменной --- полной спецификацией глобальной переменной назовем ту, в которой указано начальное значение переменной), будем называть \emph{недоспецификацией}.

Следующая спецификация также является недоспецификацией, хотя ее доопределение во многих случаях не делается:
\begin{lstlisting}
value f: Int >< Int -> Int
axiom forall x, y: Int :-
    f(x, y) is x / y pre y ~= 0
\end{lstlisting}

%"моделью" является полная спецификация..... но слово "модель" плохое, т.к. оно в русском языке используется много где. Class - это класс моделей: всевозможные доопределения до полной спецификации.

\head{Явные и неявные спецификации}

Спецификацию функции $f$ будем называть \emph{явной}, если эта спецификация имеет вид $f(x_1, x_2, ..., x_n) is e$, где $e$ --- выражение (возможно с некоторым пре-выражением). Явная спецификация дает возможность указать (явно) выражение для вычисления значения функции. Явная спецификация всегда является определением функции.

Спецификацию функции будем называть \emph{неявной}, если эта спецификация имеет вид предиката от значений входных и выходных значений функции. Неявная спецификация является определением функции только в том случае, если предикат однозначно разрешается в значения выходных данных.

Для записи неявных спецификаций используется \emph{\textbf{post}-выражение}:
\begin{lstlisting}
value f: Int >< Int -> Int
axiom forall x, y: Int :-
    f(x, y) as z  post z > 0
\end{lstlisting}
Последняя строчка является корректным \textbf{логическим} выражением в языке RSL. Оно означает, что функция f на аргументах x и y должна \textbf{завершаться детерминированно}, обозначаем z возвращенное функцией значение, и это значение должно быть положительным числом. Эта неявная спецификация не является определением, поскольку может быть доопределена до полной спецификации несколькими способами. Вот пример полной неявной спецификации:
\begin{lstlisting}
value f: Int >< Int -> Int
axiom forall x, y: Int :-
    f(x, y) as z  post z = x + y
\end{lstlisting}
Как и любое логическое выражение, post-выражение может быть помещено внутрь pre-выражения:
\begin{lstlisting}
value f: Int >< Int -> Int
axiom forall x, y: Int :-
    f(x, y) as z  post z > 0 pre x > y,
    f(x, y) as z  post z = x - y pre x <= y
\end{lstlisting}

Кроме явных и неявных спецификаций могут быть спецификации, не являющиеся явными и не являющиеся неявными (например, свойство нечетности результата не является свойством результата одного вычисления функции).

\head{Детерминированные и недетерминированные функции}

Функция называется недетерминированной, если в разных вызовах функция возвращает различное значение. Недетерминированная функция задается только при помощи следующих выражений:
\begin{enumerate}
  \item неявный let;
  \item одна из форм case (не будем вдаваться в детали, что это за форма);
  \item комбинатор недетерминированного выбора.
\end{enumerate}

Пример:
\begin{lstlisting}
value f: Int >< Int -~-> Int
axiom forall x, y: Int :-
    f(x, y) is let z : Int :- z > 0 in z end
\end{lstlisting}

Эта спецификация содержит требование того, что все возможные вычисления функции f равны всем возможным вычислениям выражения \textbf{let} z : \textbf{Int} $~\SuchAs~$ z > 0 \textbf{in} z \textbf{end} (потому что между ними находится оператор тождественности is). Неявный let возвращает произвольное значение, удовлетворяющее соответствующему предикату, недетерминированным образом. Иными словами, спецификация утверждает, что функция f должна быть недетерминированной (обратите внимание на стрелку в сигнатуре) и возвращать произвольное положительное число.

Стоит отметить, что неполное определение при помощи post-выражения не является спецификацией недетерминированной функции. Например, следующая спецификация \textbf{по определению} описывает детерминированную функцию (по определению post-выражения), просто про ее результат известно, что он положительный, но он будет ровно тем же положительным числом, если эту функцию вызывать несколько раз с одними и теми же аргументами.
\begin{lstlisting}
value f: Int >< Int -~-> Int
axiom forall x, y: Int :-
    f(x, y) as z post z > 0
\end{lstlisting}


\head{Примеры спецификаций. Краткая форма некоторых аксиом.}

Итак, спецификации (т.е. <<наборы свойств>>) бывают:
\begin{itemize}
  \item требующими тотальности / не требующими тотальности;
  \item полными / неполными;
  \item явными / неявными / просто набор аксиом.
\end{itemize}

Ряд спецификаций дают определение функции, ряд спецификаций не дают определений (просто формулируют набор свойств).

Пример тотальной полной явной спецификации функции:
\begin{lstlisting}
value add: Int >< Int -> Int
axiom forall x, y : Int :- add(x,y) is x+y
\end{lstlisting}

Это же определение удобно записывать более кратко следующим образом:
\begin{lstlisting}
value add: Int >< Int -> Int
    add(x,y) is x+y
\end{lstlisting}
Эту запись можно понимать двояко: как прототипный алгоритм вычисления функции add, и как следующее требование (или, свойство): <<функция add должна возвращать то же значение, что и значения выражения x+y>>. Важное замечание: в языке RSL тип $\Int$ включает в себя как представимые в ЭВМ целые числа, так и непредставимые. Этот факт следует учитывать при написании спецификаций.

Пример нетотальной полной явной спецификации функции:
\begin{lstlisting}
value add: Int >< Int -~-> Int
add(x,y) is x/y
\end{lstlisting}
Эта спецификация утверждает, что функция при y $\neq 0$ должна быть детерминированно завершима. При y = 0 эта функция должна вести себя так же, как вычисляется выражение x$/0$ в RSL, т.е. <<зацикливаться/падать>> (иными словами, спецификация предписывает функции <<зациклиться/упасть>>).

Пример нетотальной неполной явной спецификации функции:
\begin{lstlisting}
value add: Int >< Int -~-> Int
axiom forall x, y : Int :- add(x,y) is x/y pre y ~= 0
\end{lstlisting}
Или более кратко следующим образом:
\begin{lstlisting}
value add: Int >< Int -~-> Int
    add(x,y) is x/y
    pre y ~= 0
\end{lstlisting}

Эта спецификация требует, чтобы функция add при y $\neq 0$ детерминированно завершалась. При y = 0 эта функция может себя вести как угодно (т.е. может даже завершиться результативно, например, возвратить 0).

Еще один пример нетотальной полной явной спецификации функции:
\begin{lstlisting}
value some: Int -~-> Int
some(x) is
    local variable n:Int := x in
        while n ~= 1 do
            if n \ 2 = 0 then n := n/2
                else n := 3 * n + 1 end
        end;
        n
    end
\end{lstlisting}
Про эту функцию именно что неизвестно, завершима ли она при любом целом значении аргумента.

И еще один пример нетотальной полной явной спецификации функции:
\begin{lstlisting}
value add: Int >< Int -~-> Int
add(x,y) is x+y
\end{lstlisting}
Ничего не мешает объявить эту функцию тотальным образом, но допустимо ее определение и нетотальным (например, по причине того, что на момент написания функции неизвестно, должны ли для нее быть выполнены свойства тотальной спецификации).

Пример нетотальной неполной явной спецификации функции:
\begin{lstlisting}
value add: Int >< Int -~-> Int
add(x,y) is x/y
pre x > 2 /\ y > 4
\end{lstlisting}

Эта спецификация не запрещает вызывать функцию с аргументами, на которых \textbf{pre}-выражение ложно. Просто, для этих значений аргументов спецификация ничего не требует от функции --- она может возвращать любые значения, она может зацикливаться, она может <<падать>>, она может вести себя недетерминированно.


\subsection*{Задачи}

\input{alg/formal}

\input{basis/im2ex}


\subsection{Операции и ветви функциональности}

Данный курс посвящен формальной спецификации программно-ап-паратных систем (далее, просто <<систем>>) и их компонентов. С точки зрения пользователя система дает возможность выполнить с ее помощью ряд \emph{операций}. Аналогично, каждый отдельный компонент дает возможность остальным компонентам выполнять с его помощью ряд операций. Операция обладает рядом \emph{аргументов} и \emph{результатов операции}, непосредственно доступных тому, кто запросил данную операцию. Во время операции система (или ее отдельный компонент) ведут себя строго определенным образом в зависимости от значений аргументов, внутреннего состояния системы и состояния среды, в которой работает система (будем их называть \emph{входными параметрами} операции).

Предположим, что система еще не реализована, для нее составляется набор требований, по которым будет осуществлена реализация. От того, насколько точно будут сформулированы эти требования, будет зависеть и качество реализованной системы. Основные проблемы в требованиях следующие:
\begin{itemize}
  \item несогласованность (противоречивость): набор требований содержит как минимум несовместное подмножество требований;
  \item неполнота: набор требований ничего не говорит о том, каким должно быть поведение некоторой операции при некоторых значениях входных параметров;
  \item неоднозначность: некоторое требование можно трактовать несколькими способами.
\end{itemize}

Эти проблемы приводят в последствие к тому, что система в целом ведет себя не так, как этого хотел бы пользователем, что система вообще не может работать, поскольку при реализации ее компонентов разработчики по-разному поняли требования, что срываются сроки, отведенные на реализацию, нарушается бюджет проекта и т.д. и т.п.

В качестве одного из методов обнаружения и избавления от таких проблем в данном курсе рассматриваются формальные спецификации. Идея заключается в том, что разработчик требований должен составить одну или несколько \emph{формальных моделей} поведения компонентов и системы (под \emph{поведением системы} понимается .........., для краткости будем называть \emph{поведением операции} поведение системы при выполнении операции). Такие модели дают однозначное задание поведения с возможностью применения математических методов для выяснения наличия противоречий и неполно описанных требований. В очень простых случаях такие формальные модели могут стать основой для реализации систем, но в общем случае сложность системы не позволяет получить такую модель. Вместо этого создают несколько небольших формальных моделей, описывающих поведение системы с отдельных точек зрения, игнорируя ряд деталей. Процесс создания формальной модели будем называть \emph{уточнением требований}, поскольку модель составляется, исходя из некоторого неформального представления о поведении системы, а в результате построения формальной модели получается однозначное, формальное, описание поведения системы.

Каждой операции сопоставим отдельную функцию на RSL с определенной сигнатурой:
$$op : S \times I ~\NonDetermFn~access~ S \times O$$
где $S$ --- состояние системы (слева от стрелки это состояние до выполнения операции, \emph{пре-состояние}, справа от стрелки это состояние после выполнения операции, \emph{пост-состояние}), $I$ --- аргументы операции, $O$ --- результаты операции (та информация, которая становится известной/актуальной только после выполнения операции), $access$ --- указание глобальных переменных, к которым осуществляется доступ в рамках выполнения операции.

Назовем класс значений входных параметров операции, при котором ее поведение с некоторой точки зрения одинаковое, \emph{ветвью функциональности} операции. Например, операция добавления элемента в список работает по-разному, если список пустой и если список непустой (в первом случае создается новый <<объект>>-список, во втором случае --- не создается, только происходит дополнение его элементов). Поэтому для этой операции можно выделить такие две ветви функциональности: при пустой списке и при непустом списке.

Ветви функциональности можно получать следующим \emph{комбинаторным способом}. Для операции выделяется набор элементарных характеристик, обладающих конечным числом значений. В каждой ветви функциональности каждая характеристика обладает своим значением, а каждая ветвь функциональности представляется вектором значений, отдельные элемент такого вектора соответствует отдельной характеристике.

При некоторых значениях входных параметров операция может быть не определена (например, операция нахождения максимального элемента в списке не определена для пустого списка). Такие входные параметры мы в дальнейшем будем выделять особо и не называть их ветвями функциональности.


%понятие предусловия, постусловия:
%
%[Большая цитата из статьи В.Кулямина, 14(1)й том трудов ИСП]
%
%Программный контракт операции состоит из предусловия и постусловия. Первое фиксирует требования к корректному использованию этой операции со стороны окружения системы — при каких ограничениях на аргументы обращение к этой операции корректно. Второе определяет обязательства системы по отношению к результатам вызовов этой операции — какие ограничения на результаты работы операции должны быть выполнены при корректной работе системы, если обращение к ней было правильным. При нарушении предусловия операции обращение к ней может иметь любые последствия, поведение системы в этом случае не определено. Совместно пред- и постусловия строго определяют требования к работе системы.
%
%При анализе сложной системы с большим количеством интерфейсных операций крайне неудобно рассматривать их все вместе как однородный набор, необходимо разбиение этих операций на какие-то логические группы по реализуемым ими функциям. Эти группы почти всегда соответствуют компонентам или модулям системы, ответственным за реализацию этих функций. Часто такие компоненты имеют внутреннее состояние, недоступное для непосредственного наблюдения извне системы, но влияющее на поведение вызываемых операций компонента и изменяемое ими.
%
%Поэтому для описания ограничений в пред- и постусловиях необходимо как-
%то учитывать внутреннее состояние компонента, операции которого
%описываются. Чтобы сделать это возможным, контракты операций одного
%компонента объединяются в спецификацию этого компонента вместе с
%описанием структуры его модельного состояния.
%Структура модельного состояния компонента не обязана совпадать со
%структурой его реального состояния, зафиксированной в его коде, например,
%компонент, реализующий список, может использовать ссылочную структуру
%данных, в том время, как структура его модельного состояния в
%спецификациях может быть основана на массиве. В структуре модельного
%состояния могут совсем отсутствовать некоторые части реального состояния
%компонента, слабо связанные с его функциональностью, например,
%различного рода кэши и другие данные, используемые для увеличения
%производительности. Важно, что структура модельного состояния компонента
%должна содержать данные, достаточные для полного описания
%функциональности в пред- и постусловиях операций этого компонента. При
%этом предусловие зависит от аргументов вызова операции и данных
%модельного состояния при этом вызове, или пре-состояния. Постусловие
%зависит как от аргументов и пре-состояния, так и от результата и данных
%модельного состояния после вызова, или пост-состояния.
%Наличие сложной структуры модельного состояния приводит к
%необходимости учитывать в контрактах операций ограничения на его данные,
%которые должны выполняться в стабильных состояниях системы, когда ни
%одна из операций не выполняется. Такие ограничения оформляются в виде
%инвариантов модельного состояния. Инварианты являются общими частями
%пред- и постусловий всех операций, как-то затрагивающих соответствующие
%компоненты — они должны выполняться как в пре-состоянии любого вызова,
%так и в его пост-состоянии.
%
%
%Обычно постусловие операции описывает несколько разных режимов ее
%функционирования. Предусловие запрещает все комбинации значений
%параметров, при которых поведение операции не определено. Однако среди
%разрешаемых предусловием ситуаций могут остаться такие, в которых
%выполнить свою основную функцию операция не может. Вместо этого она
%должна вернуть некоторый код ошибки, создать исключительную ситуацию
%или как-то иначе сигнализировать о том, что ее основная задача не может
%быть решена в такой ситуации. Помимо режимов сигнализации о
%невозможности выполнить основную функцию, само ее выполнение может
%идти разными путями. Например, операция конкатенации двух строк может
%проверять, не является ли один из ее аргументов пустой строкой, и в этом
%случае просто возвращать копию другого аргумента, не выполняя никаких
%действий над ней. Если же оба аргумента не пусты, копия одного из них
%должна быть подвергнута модификации, чтобы получить результат операции.
%
%При написании постусловий удобно выделять такие разные режимы, иначе
%постусловие превращается в большую и сложную формулу, трудную для
%анализа и понимания, что противоречит основной цели создания формальных
%спецификаций. Различные режимы работы операции описываются в виде
%импликаций с несовместными посылками (постусловие при этом выглядит как формула
%(X1 => Y1) /\ (X2 => Y2) /\ ... (Xn => Yn)
%или в виде разных выражений для
%возвращаемого результата при разных исходных условиях, т.е. результат
%постусловия вычисляется в разных ветвях некоторого условного оператора
%или оператора выбора по-разному. Поэтому эти разные режимы называют
%ветвями функциональности (или функциональными ветвями) операции.

\subsection*{Задачи}

\zhead{Составить сигнатуры функций и выделить ветви функциональности каждой из них}

..............TODO


%\section*{Заключение}
%Дальнейшее рассмотрение касается спецификации функций, оперирующих с более сложными типами данных, нежели числа, символы и булевы значения (например, такие типы данных возникают при спецификации состояний программных компонентов). Существуют различные \emph{стили специфицирования}, т.е. методы определения сложных типов данных и операций над ними, дающие аксиомы специального вида, и различное применение спецификаций. Рассматриваемые в данном задачнике методы применяются в тех случаях, когда требуемая функциональность достаточно сложная, имеется большое количество требований к тому, как должны работать последовательные программные компоненты.

\pagebreak
\section{Уточнение требований при помощи формальных моделей}

Как сказано в предыдущем разделе, уточнение требований выполняется путем выделения ветвей функциональности, т.е. классов значений входных параметров. В данном разделе предлагается использовать язык множеств, списков и отображений для описания типов параметров и выражений над значениями параметров. При этом для описания ветвей функциональности отдельных операций будет применяться явное или неявное описание. В данном случае оно называется \emph{моделеориентированным} описанием (потому что для параметров задается <<модель>> на языке множеств, списков и отображений).

\input{model/setlist}  % with problems

\subsection{Моделеориентированные спецификации}

.............TODO предусловие, запись в явном или неявном виде, замкнутое описание (включает ли выходное состояние....), инвариант.......

.....TODO первая задачка экзамена




\section{Уточнение требований при помощи алгебр}

\subsection{Алгебраические спецификации}

Если количество состояний системы невелико, систему удобно моделировать в виде конечного автомата\footnote{вспомните курс <<Объектно-ориентированного анализа и проектирования>>}. При возрастании количества состояний конечные автоматы становятся неудобными как для моделирования, так и для работы с такими моделями. До некоторого момента и для некоторых задач помогают расширенные конечные автоматы (EFSM), модели Крипке, но для систем более реальных размеров и они могут стать неудобными. Тогда вместо такого (явного) указания состояний и переходов между ними предлагается задавать \emph{правила}: о структуре состояния, о свойствах состояния, о свойствах переходов\footnote{Аналогично совершается переход от задания формальных языков перечислением его слов к формальным грамматикам, т.е. правилам конструирования слов}. Одним из основных механизмов теперь будет логический вывод новых свойств и правил из заданных в спецификации.

\input{alg/theor}

\section*{Задачи}

\input{alg/calc}

\input{alg/find_errors}

\input{alg/unformal}

\input{alg/problems}

\subsection{Полнота и непротиворечивость алгебраических спецификаций}

\input{alg/compness}

\section*{Задачи}

\input{alg/comprobs}

\input{alg/fsm}

%%%% отнести это в раздел "Дополнительно" ?
\subsection{Cпецификация рекурсивных типов}

%\head{Рекурсивное определение типов (деревьев)}
Алгебраические модели и АТД являются удобным способом рекурсивного задания типов и операций их обработки. Для этого представленный только что формальный метод построения достаточно полных алгебраических спецификаций прочитывается следующим способом:
\begin{enumerate}
  \item выделить и составить сигнатуры конструкторов (пустое значение | составление нового <<узла дерева>>);
  \item выделить и составить сигнатуры функций-обработчиков рекурсивного типа;
  \item описать результат обработки для каждого конструктора.
\end{enumerate}

Например, спецификация функции, вычисляющей глубину бинарного дерева, согласно этому методу получается такой:
\begin{lstlisting}
type Node, Tree == empty | mk_tree(Node, Tree, Tree)
value depth: Tree -> Nat
axiom forall n: Node, left: Tree, right: Tree :-
  depth( empty ) is 0,
  depth( mk_tree(n, left, right) ) is
          max( depth(left), depth(right) )
value max: Nat >< Nat -> Nat
   max(x,y) is if x > y then x else y end
\end{lstlisting}

Конструктор предназначена лишь для структурных целей, т.е. определение дерева в виде типа Tree из этого примера пойдет и для бинарного дерева произвольного вида, и для бинарного сбалансированного дерева, и для других бинарных деревьев. А уже менее тривиальные функции составления деревьев (например, чтобы не нарушалась сбалансированность) определяются в виде функций-обработчиков.

\section*{Задачи}
%
\zhead{}%Рекурсивные типы}
%
\z Специфицируйте операцию проверки вхождения элемента в бинарное дерево.

\textbf{Решение:}
\begin{lstlisting}
type Node, Tree == empty | add(Node, Tree, Tree)
value check: Node >< Tree -> Bool
axiom forall n, n1:Node, left, right: Tree :-
   ~check( empty ),
   check(n, add(n1,left,right) ) is (n = n1) \/
             check(n, left) \/ check(n, right)
\end{lstlisting}

\z Специфицируйте операцию вычисления высоты бинарного дерева.

\z Специфицируйте операцию проверки бинарного дерева на сбалансированность.

\z Специфицируйте операцию получения предка элемента бинарного дерева.

\z Специфицируйте добавление элемента в двоичное дерево поиска.

\z Специфицируйте удаление элемента из двоичного дерева поиска.

\z Специфицируйте добавление элемента в АВЛ-дерево. Определение операции предполагается найти самостоятельно.

\z Специфицируйте удаление элемента из АВЛ-дерева. Определение операции предполагается найти самостоятельно.

\z Специфицируйте добавление элемента в 2-3-дерево. Определение операции предполагается найти самостоятельно.

\z Специфицируйте удаление элемента из 2-3-дерева. Определение операции предполагается найти самостоятельно.

\z Специфицируйте добавление элемента в декартово дерево. Определение операции предполагается найти самостоятельно.

\z Специфицируйте удаление элемента из декартова дерева. Определение операции предполагается найти самостоятельно.

\z Специфицируйте добавление элемента в красно-чёрное дерево.  Определение операции предполагается найти самостоятельно.

\z Специфицируйте удаление элемента из красно-чёрного дерева.  Определение операции предполагается найти самостоятельно.

% специфицировать стратегии вытеснения



%\chapter{Моделе-ориентированные спецификации}

Моделе-ориентированные спецификации, как и алгебраические, описывают семантику интерфейсов программных компонент. Они основываются на \emph{абстракции алгоритмов} и \emph{абстракции данных}.

Абстракция алгоритмов предполагает, что для функций задаются (\emph{специфицируются}) не алгоритмы, их реализующие, а дается определение осуществляемого функцией отображения входных данных на выходные. Для этого зачастую используется аппарат \emph{программных контрактов}.

Абстракция данных предполагает, что для состояния компонента и типов параметров функций компонента (входных и выходных) указывается не их выражение в терминах целевого языка программирования (или их эквивалентов), а смысл, семантику этих данных, исходя из логического содержания и требований на внутренние отношения составляющих частей состояния. Например, если эти части \emph{<<по логике>>} должны быть неупорядочены и без повторов, то для моделирования таких частей следует использовать \emph{множества}. Если важен порядок и возможны повторы, то \emph{списки}. Если логически выделяются отображение одних данных в другие (отображение ключа в данные), то \emph{отображения}. Отображения являются наиболее адекватным представлением данных, которые по сути представляются <<реляционным отношением>> с первичным ключом.

В тексте реализации типы (наверняка) будут иметь другое представление, адекватное языку программирования (например, если система реализуется на Си, то вместо множеств или списков будут указатели), но логически функция в реализации должна принимать те же параметры (синтаксически функции передается указатель, а на самом деле этот указатель будет обозначать множество или список) и осуществлять то же отображение входных на выходные параметры, как это указано в спецификации.

\section{Моделирование данных}

При определении типов данных используются встроенные типы и подтипы определенных ранее типов. Подтип наследует все операции своего \emph{максимального} типа (типа-<<предка>>), но множество его значений может быть уже множества значений максимального типа. Часто в виде максимальных типов задается структура данных без сложных внутренних семантических ограничений, а затем определяются подтипы этих типов, множество значений которых составляют уже только семантически корректные значения максимального типа.

Подтип может быть оформлен в разделе type следующим образом:
\begin{lstlisting}
type Nat3 = {| n : Nat :- n isin {1..3} |}
\end{lstlisting}

или с помощью аксиом:
\begin{lstlisting}
type Nat3 = Nat
axiom all n : Nat3 :- n isin {1..3}
\end{lstlisting}

Обратите внимание, что тип (или его подтип) --- не есть множество (-set).

Учтите, что модель данных не должна содержать <<реализационных решений>>, т.е. она должна отражать лишь то, что перечислено в требованиях к данным и операциям, и должно оставлять свободу для дальнейшего уточнения и принятия конструкторских решений при реализации системы в рамках спецификации.

При выборе модели следует руководствоваться следующими соображениями:
\begin{enumerate}
  \item \textbf{естественность}: модель должна выражать свойства так, как пришло бы в голову любому <<нормальному>> человеку;
  \item \textbf{удобство} описания функциональности, описания требований и последующее чтение этих требований с целью ознакомления, понимания;
  \item \textbf{отсутствие реализационных, проектных, решений}.
\end{enumerate}

\section*{Задачи}

\zhead{Промоделировать указанные данные}

\z <<Крестики-нолики>>. Промоделировать игровое поле 3х3 в игре <<крестики-нолики>>.

\textbf{Решение}

Рассуждаем о состоянии, о его частях и об отношениях этих частей (заметьте, что эти рассуждения носят не реализационный, а логический характер!). Игровое поле состоит из клеток, клетки рассматриваются как элементы строк и как элементы столбцов.

\begin{lstlisting}
type Cell == empty | cross | outh,
        Field = (Nat >< Nat) -m-> Cell
axiom all f: Field :-
   dom f = {(n1, n2)| n1 : Nat, n2: Nat :- {n1,n2} <<= {1..3}}
\end{lstlisting}

\z <<Крестики-нолики>>. Промоделировать игровое поле 3х3 в игре <<крестики-нолики>>, возможное во время игры.

\z <<Турнир по круговой схеме>>. Все участники играют одинаковое число партий (туров), встречаясь между собой по схеме <<каждый с каждым>>. По результатам каждой партии участнику начисляется определённое количество очков. Например, в шахматах традиционно начисляют 1 очко за выигрыш, 0 очков за проигрыш и 0,5 очка за ничью. Очки, набранные участниками в течение всего турнира, суммируются. Места распределяются по убыванию количества набранных очков.

\z <<Турнир по олимпийской системе (плей-офф)>>. Количество участников розыгрыша плей-офф обязательно должно быть степенью двойки (2, 4, 8, 16, 32 и так далее). Двоичный логарифм числа участников определяет число кругов розыгрыша (туров). Общее число игр на единицу меньше числа участников. Круги розыгрыша обычно называются по количеству пар участников: для 1 пары — <<финал>> (он определяет победителя), для 2 пар — <<полуфинал>>, для 4 пар — <<четвертьфинал>> и так далее. В каждом круге из участников составляются пары, играющие между собой (ничьих быть не может). Из каждой пары в следующий круг выходит победитель, а побеждённый выбывает из турнира. Участник, выигравший финальный круг, становится победителем, его последний соперник получает второе место. За третье место проводится дополнительный матч между двумя участниками, проигравшими в полуфинале.

\z <<Генеалогическое дерево>>. Каждый человек имеет не более двух родителей. Родители каждого человека имеют разный пол. Каждый человек младше каждого из своих родителей. Даты жизни родителей каждого человека пересекаются. В корне дерева стоит один человек.

\z <<Разбиения>>. Разбиение --- это непустая коллекция взаимноразличных, непустых коллекций значений типа A.
\begin{itemize}
  \item  <<Сильносвязное разбиение>> --- это множество множеств, любой элемент которого обладает не более чем одним значением, которое присутствует во всех остальных элементах;
  \item <<$n$--связное разбиение>> --- это множество множеств, любой элемент которого обладает не более чем одним значением, которое присутствует ровно в $n$ остальных элементах;
  \item <<Кольцевое разбиение>> --- это множество множеств, чьи элементы (разбиения) можно расположить в виде кольца, в котором совпадающими элементами обладают только соседние элементы разбиения.
\end{itemize}

\z <<Тезаурус>>. Это набор групп слов с похожим значением. В тезаурусе не может быть слов, которые появились бы более чем в одной коллекции.

\z <<Заказ билетов на поезд>>. Есть станции, поезда и маршруты (последовательности станций). Билеты можно заказывать как целиком на весь маршрут, так и на его часть. Все поезда, на которые можно заказывать билеты, должны быть известны системе (помещаться в структуре о поездах). Все места для заказа действительно присутствуют в поезде. Нельзя иметь два различных заказа одного и того же места в том же самом поезде для какой-либо части маршрута поезда.

\z\footnote{Задача взята из~\cite{ModellingSystems}} The system to be modelled is part of a controller for a robot that positions explosives such as dynamite and detonators in a store. The store is a rectangular building. Positions within the building are represented as coordinates with respect to one corner designated the origin. The store’s dimensions are represented as maximum x and y coordinates. Objects in the store are rectangular packages, aligned with the walls of the store. Each object has dimensions in the x and y directions. The position of an object is represented as the coordinates of its lower left corner. All objects must fit within the store and there must be no overlap between objects.

\z\footnote{Задача взята из~\cite{ModellingSystems}} Each message is a non-empty sequence of characters starting with the sequence “STR” and ending with the sequence “STP”. The total length of a message must not exceed 10000 characters.  A message is defined as high security if it contains an occurrence of the string “SECRET”. If it does not contain the string “SECRET” and it does contain the string “UNCLASSIFIED” then the message is treated as low-security. If neither string is present, then the message is classes as high-security.

\z <<Военная система>>. Подчиненные, единственный генерал, у солдат нет подчиненных. воинского подразделения. Иерархия должна удовлетворять следующим ограничениям:
\begin{itemize}
  \item военнослужащие могут иметь только следующие звания (в порядке возрастания старшинства):
    \begin{itemize}
        \item рядовой солдат (soldier);
        \item лейтенант (lieutenant);
        \item капитан (captain);
        \item майор (major);
        \item полковник (colonel);
        \item генерал (general)
    \end{itemize}
  \item у каждого военнослужащего, за исключением рядовых солдат, есть подчиненные;
  \item у каждого военнослужащего, за исключением генералов, есть командир, причем ровно один, звание которого выше звания военнослужащего;
  \item все непосредственные подчиненные одного военнослужащего имеют одинаковые звания;
  \item во главе подразделения стоит один военнослужащий -- у него нет командиров.
\end{itemize}

\z <<SMS-база>>. SMS обладает текстом и номером, кому она отправлена. Кроме того, у SMS есть идентификатор, он присваивается в момент регистрации SMS, чтобы идентифицировать SMS с одинаковым текстом и изначально его нет. Кроме того, у SMS есть статус (например, обработана/не обработана). Статус может меняться. Задача состоит в том, чтобы описать термины <<SMS>> и <<база SMS>> с учетом удобства формализации упомянутых операций.

\z <<Кэш-память>>. Кэш-память состоит из секций. Секции состоят из строк. Каждая строка кэш-памяти состоит из одних и тех же полей. Длина строки и количество строк в секции фиксированы для кэш-памяти. Среди полей есть поле <<тег>>. Для строк с одним и тем же номером в секции не должно быть одинаковых тегов. Задача состоит в том, чтобы описать кэш-память с учетом удобства поиска строки по тегу и изменения полей строки по тегу.

\z <<Код Хаффмана>>. Опишите корректную таблицу соответствия символов и их кодов, получаемых согласно алгоритму Хаффмана\footnote{определение взято из свободной энциклопедии Википедии}: на основе таблицы частот встречаемости символов в сообщении строится дерево кодирования Хаффмана (Н-дерево) следующим образом:
\begin{enumerate}
  \item Символы входного алфавита образуют список свободных узлов. Каждый лист имеет вес, который может быть равен либо вероятности, либо количеству вхождений символа в сжимаемое сообщение.
  \item Выбираются два свободных узла дерева с наименьшими весами.
  \item Создается их родитель с весом, равным их суммарному весу.
  \item Родитель добавляется в список свободных узлов, а двое его детей удаляются из этого списка.
  \item Одной дуге, выходящей из родителя, ставится в соответствие бит 1, другой — бит 0.
  \item Шаги, начиная со второго, повторяются до тех пор, пока в списке свободных узлов не останется только один свободный узел. Он и будет считаться корнем дерева.
\end{enumerate}

Чтобы определить код для каждого из символов, входящих в сообщение, мы должны пройти путь от листа дерева, соответствующего этому символу, до корня дерева, накапливая биты при перемещении по ветвям дерева. Полученная таким образом последовательность битов является кодом данного символа, записанным в обратном порядке.

\z <<Куча>> --- двоичное дерево с ключами в вершинах, в котором ключ вершины должен быть строго больше ключей ее непосредственных сыновей.

\z <<Дерево поиска>> --- двоичное дерево с ключами в вершинах, в котором ключ вершины должен быть строго больше ключей ее непосредственных сыновей левого поддерева и строго меньше ключей ее непосредственных сыновей правого поддерева.

\z <<Декартово дерево>> (Treap) --- дерево, в вершинах которого хранятся пары ключей (x, y), причем
по первым компонентам пар (<<ключам>>) дерево является деревом поиска, а по вторым компонентам пар (<<приоритетам>>) --- кучей. В русскоязычной литературе эту структуру данных также называют <<дерамидой>> (дерево + пирамида) или <<дучей>> (дерево + куча). Дерево именуется декартовым, поскольку его легко представить на декартовой плоскости, используя пары ключей как координаты вершин (абсцисса, ордината).

% еще можно набрать задач отсюда: http://informatics.mccme.ru/moodle/course/view.php?id=18

%%\z Формализуйте определения терминов, приведенных в этом тексте --- они выделены курсивом (он взят из~\cite{structures_algorithms}). \emph{Дерево} --- это совокупность элементов, называемых \emph{узлами} (один из которых определен как \emph{корень}), и отношений (<<родительских>>), образующих иерархическую структуру узлов. Узлы, так же, как и элементы списков, могут быть элементами любого типа. Мы часто будем изображать узлы буквами, строками или числами. Формально дерево можно рекуррентно определить следующим образом.
%%\begin{enumerate}
%%\item Один узел является деревом. Этот же узел также является корнем этого дерева.
%%\item Пусть $n$ --- это узел, а $T_1, T_2, ..., T_k$ --- деревья с корнями $n_1, n_2, ..., n_k$ соответственно. Можно построить новое дерево, сделав $n$ родителем узлов $n_1, n_2, ..., n_k$. В этом дереве $n$ будет корнем, а $T_1, T_2, ..., T_k$ --- \emph{поддеревьями} этого корня. Узлы $n_1, n_2, ..., n_k$ называются \emph{сыновьями} узла $n$.
%%\end{enumerate}
%%
%%Часто в это определение включают понятие \emph{нулевого дерева}, т.е. <<дерева>> без узлов.
%%

\zhead{Составление модели данных\footnote{Текст требований взят из методического пособия А.В.Чернова к практикуму по курсу <<Операционные системы>>}}

Составьте и формализуйте модель данных, достаточную для спецификации указанного набора операций. Обратите внимание, что <<за скобками>> требований к этим операциям остается та информация, которая позволяет описать функциональность этих операций, описать то, как они изменяют соответствующие данные. Ваша задача --- вычленить и должным образом оформить такие данные. Избегайте реализационных решений, помните об естественности и удобстве.

\z Операции распределения динамической памяти: malloc, realloc, free и разыменование указателя. Вот лишь ряд требований, которые должны естественно выражаться на искомой модели данных:
\begin{enumerate}
  \item malloc выделяет область памяти заданного размера и возвращает указатель на начало этой области памяти;
  \item при невозможности выделения памяти malloc возвращает специальное значение NULL;
  \item free освобождает ранее выделенный блок памяти и делает его доступным для повторного использования;
  \item переданный free указатель, должен быть получен от malloc или realloc; иначе результат работы этой функции неопределен;
  \item если блок памяти был уже освобожден, результат повторного его освобождения с помощью free не определен;
  \item после того, как блок памяти освобожден, с ним нельзя проводить никаких операций, даже разыменование;
  \item вызов free(NULL) безопасен и не приводит ни к каким действиям;
  \item free не требует указывать ей размер освобождаемой памяти, освобождается вся память, выделенная ранее с помощью malloc или realloc;
  \item realloc принимает на вход указатель на область памяти и (новый) размер;
  \item если realloc передан размер, равный нулю, то она работает как free, если передан указатель NULL, то она работает как malloc;
  \item в остальных случаях realloc выделяет в динамической памяти блок заданного размера и копирует в его начало данные по переданному ей указателю; старый блок памяти становится недоступным для операций с ним;
  \item если новый блок больше старого, оставшиеся данные не инициализируются;
  \item не гарантируется, что новый блок будет начинаться с того же адреса памяти, что и старый;
  \item если невозможно выделить новую память, realloc возвращает NULL; в этом случае память по старому адресу не изменяется и остается доступной.
\end{enumerate}

%\z Send, receive

\z Операции с файлами: open, read, write, close. Вот лишь ряд требований, которые должны естественно выражаться на искомой модели данных:
\begin{enumerate}
  \item \texttt{FILE open(name, mode)} открывает файл с именем name в режиме mode;
  \item если mode = read, то файл открывается для чтения; текущая позиция в файле устанавливается на начало файла;
  \item если mode = write, то файл открывается для записи; если файл не существовал, он создается; текущая позиция в файле устанавливается на начало;
  \item если файл открыт успешно, возвращается некая структура FILE, в противном случае константа NULL;
  \item \texttt{close(FILE)} закрывает файл; дальнейшие операции с ним невозможны;
  \item \texttt{int read(buffer, sizeofbuffer, FILE)} считывает данные из файла FILE в буфер buffer, не более sizeofbuffer байтов; возвращает количество успешно считанных байтов;
  \item \texttt{int write(buffer, sizeofbuffer, FILE)} записывает данные в файл FILE из буфера buffer, не более sizeofbuffer байтов; возвращает количество успешно записанных байтов.
\end{enumerate}

\z Операции с процессами: fork, exec, getpid, exit. Вот лишь ряд требований, которые должны естественно выражаться на искомой модели данных:
\begin{enumerate}
  \item \texttt{int fork()} создает новый процесс;
  \item созданный с помощью fork процесс отличается от создававшего только идентификатором процесса и идентификатором процесса-родителя;
  \item сыновний процесс продолжает выполнять тот же код, что и процесс-родитель;
  \item в сыновний процесс fork возвращает 0, в родительский --- идентификатор созданного потомка, если тот создался успешно, или -1, если сыновний процесс создать невозможно (нехватка ресурсов или превышение разрешенного числа процессов);
  \item \texttt{int getpid()} возвращает идентификатор текущего процесса;
  \item если при создании сыновнего процесса идентификатор достиг заданной верхней границы, счёт идентификаторов начинается с единицы;
  \item \texttt{int exec(path)} замещает тело процесса (содержимое кода, данных и стека) содержимым файла по пути path;
  \item загружаемая программа наследует идентификатор процесса;
  \item в случае ошибки exec возвращает -1;
  \item в случае успеха управление в первоначальную программу не возвращается;
  \item \texttt{exit(status)} завершает работу процесса с кодом завершения status;
  \item соглашение о взаимодействии процессов предполагает, что код завершения 0 означает успешное завершение процесса, а все прочие --- неуспешное.
\end{enumerate}


\section{Программные контракты}

Программный контракт операции состоит из ее предусловия и постусловия. Предусловие (по Майеру) --- это условие, определяющее те входные данные операции, на которых гарантируется выполнение постусловия --- заданного условия на входные и выходные данные операции. Обратите внимание, что программный контракт есть указание свойств результата операции, а не алгоритма его вычисления.

Для того, чтобы выразить на RSL предусловие некоторой операции, нужно определить подтип типа её входного аргумента. Например, в следующем примере для операции целочисленного деления указано предусловие, гарантирующее завершение вычисления этой операции:
\begin{lstlisting}
type TwoNumbers = Int >< Int
axiom all n: TwoNumbers :-
  let (n1,n2) = n in n2 ~= 0 end
value division: TwoNumbers -> Int
\end{lstlisting}

Обратите внимание, что этой функции дается \textbf{тотальное} определение, потому что для всех допустимых значений ее аргументов она должна завершаться и давать детерминированным образом результат.

Не у всех операций должны быть предусловия. <<Публичные>> функции, функции, которые можно вызывать из любых состояний и с любыми значениями входных параметров (и это записано в спецификации, что должна иметься возможность вызывать эту функцию при любых входных параметрах), не должны иметь предусловий. В них надо описать все случаи, когда функция должна себя вести неким определенным образом, описать условия на входные параметры, при которых возникает каждый из этих случаев, и описать результат функции во всех выделенных случаях.


\head{pre-выражения и post-выражения, explicit и implicit определения функций}

\emph{Explicit (явное) определение} функции имеет вид (без указания побочного эффекта):
\begin{lstlisting}
value name : parameters -> parameters
name(parameters_names) is expression
\end{lstlisting}

Возможно как тотальное, так и нетотальное определение.

Явное определение позволяет указать выражение для вычисления результата функции по входным данным. Оно полезно в тех случаях, когда результат описывается формулой небольшой длины от входных параметров функции.

Explicit (явное) определение функции c \emph{pre-выражением} имеет вид:
\begin{lstlisting}
value name : parameters -> parameters
name(parameters_names) is expression
pre logic_expression
\end{lstlisting}

Возможно как тотальное, так и нетотальное определение. logic\_expression не должно содержать побочный эффект.

Для значений входных данных, на которых logic\_expression истинно, функция должна возвращать тот же результат, как и expression. Про результат работы функции на остальных значениях входных данных такое определение функции ничего не говорит: функция остается \emph{недоспецифицированной}. Для указания результата работы функций в этих случаях можно написать несколько аксиом, повторное же явное определение функции с другим pre-выражением в RSL недопустимо.

\emph{post-выражение} позволяет описать <<эффект>> вычисления некого выражения (как связаны состояние глобальных переменных до вычисления выражения и после вычисления выражения, значения переменных выражения и значение этого выражения). Синтаксис post-выражений следующий:
\begin{lstlisting}
expression [as binding] post logic_expression
\end{lstlisting}

В logic\_expression должен отсутствовать побочный эффект. post-выражение само по себе явлется логическим выражением. Оно истинно, если expression завершилось (и получено единственное значение для binding) и по результатам его выполнения истинно logic\_expression.

Например:
\begin{lstlisting}
  (x := x+1; x := x+2; x) as a post (a = x /\ x = x'+3)
\end{lstlisting}
После вычисления выражения (x := x + 1; x := x + 2; x) для нового значения переменной x (х) и старого значения переменной х (x') должно быть выполнено условие (x = x' + 3). Именем <<a>> названо значение выражения (x := x + 1; x := x + 2; x) --- оно равно значению выражения <<x>>. Если expression имеет тип $\Unit$, то в post-выражении не может быть записи <<as binding>>.

Еще пример:
\begin{lstlisting}
  (x := x + 1; x := x + 2) post (x > x')
\end{lstlisting}
Выражение слева от $\Post$ то же, что и в первом примере, но другое проверяемое условие.

%post-выражение может использоваться для указания области детерминированной завершимости функции: ...........

\emph{Implicit (неявное) определение} функции имеет вид:
\begin{lstlisting}
value name : parameters -> parameters
name(parameters_names) [as binding] post logic_expression
\end{lstlisting}

Оно является сокращением аксиомы
\begin{lstlisting}
value name : parameters -> parameters
axiom all parameters_names : parameters :-
name(parameters_names) [as binding] post logic_expression
\end{lstlisting}

Возможно как тотальное, так и нетотальное определение.

Implicit (неявное) определение функции с pre-выражением имеет вид:
\begin{lstlisting}
value name : parameters -> parameters
name(parameters_names) [as binding] post logic_expression
pre logic_expression
\end{lstlisting}

Как и для явного задания, pre-выражение ограничивает входные данные, на которых <<действует>> данное неявное задание.

Важно понимать, что \textbf{pre-выражение не задает предусловие операций}. Оно задает область, в которой нечто утверждается.

Заметьте, что <<явное>> или <<неявное>> --- речь идет об определении, но не о самой функции, поскольку способов задать, определить, функцию может быть много, но все они будут <<говорить>> об одной и той же сущности, об одной и той же функции.

% если вызывается функция с аргументами, не попадающими в область своих типов, то как себя ведет функция ?
% -> если такое возможно в спецификации, то в ней найдена ошибка
% если вызывается функция с аргументами, не попадающими в пре-выражение, то как себя ведет функция ?
% -> как угодно, мы еще не специфицировали, как она должна себя вести на этих аргументах
%    если такое возможно в спецификации, то она неполна

\head{Недоспецификация, уточнение спецификаций}

Практически всегда невозможно при написании первой спецификации точно указать все различные случаи, в которых поведение специфицируемой функции будет особым. Например, если специфицируется компонент, осуществляющий кэширование данных, то сначала известно лишь то, что этот компонент хранит некие специальные данные, но неизвестно, например, какое хранение будет согласованным, как компонент будет реагировать на переполнение. Однако даже не зная ответов на эти вопросы, можно и нужно писать первые спецификации. Затем уже будут подготовлены следующие версии спецификации, уточняющие предыдущие. При этом про первые спецификации говорят, что они являются \emph{недоспецификациями}. Недоспецификация превращается в полную спецификацию при уточнении и дополнении состояния компонента: в первых спецификациях была известна лишь его часть (как структурная, так и семантическая). Например, не было учтено, что при кэшировании для каждой порции данных хранится время ее жизни в кэше, а без этого нельзя точно сказать, какие порции данных надо вытеснить из кэша при его переполнении.

Для оформления недоспецификаций очень удобно использовать post-выражения, т.к. зачастую достоверно неизвестно, как строить единственное возвращаемое значение по данному небольшому набору известных в данной спецификации входных данных.


\head{Советы по написанию постусловий}

Здесь описан ряд технических замечаний, советов по тому, как, о чем, думать при написании постусловий на RSL, чтобы они получались короче, яснее, были бы более удобными для последующей работы с ними.

RSL позволяет описывать меньший список через большой. Если функция f принимает на вход список x и возвращает список f(x) меньшей длины, то описываем f(x) через перебор элементов х. Если f(x) больше x, то описываем x через перебор элементов f(x):
\begin{lstlisting}
f(x) as y post x = <. t | t in y :- p(t).>
\end{lstlisting}

При спецификации функций, генерирующих одни множества по другим, полезно специфицировать пересечения и разницы этих множеств (пересечение задаст постоянную часть множества, разница множеств --- меняющуюся часть):
\begin{lstlisting}
f(x) as y post (x inter y is ...) /\ (y \ x is ... )
\end{lstlisting}

Операторы inds, hd и tl используйте тогда, когда не помните, с <<1>> или с <<0>> считаются индексы в списке. Кроме того, оператор inds дает дополнительную подсказку при чтении, что соответствующая переменная является индексом:
\begin{lstlisting}
f(x) as y post ... (all i:Nat :- i isin inds y => y(i+1)>y(i))
\end{lstlisting}

Композиция отображений --- это способ построить выборку по двум критериям.
%% что это значит ??

Не бояться использовать бесконечные сущности в спецификации.

Применять схемы сокращения записи в случае требований выполнения/невыполнения нескольких условий одновременно.

Если для структуры данных нужно делать поиск и добавление в нее новых данных, то для ее моделирования лучше всего использовать отображение. Критерий поиска становится ключом, а добавляемые элементы --- значениями.

\head{Советы по получению понятных спецификаций}

\begin{itemize}
    \item Выбирать <<говорящие>> имена для параметров, функций, имен переменных и типов.
    \item Строить дополнительные функции, позволяющие <<читать>> выражения, в которых они встречаются.
    \item Выбирать одну из наиболее коротких форм записи выражений.
\end{itemize}

Пример: специфицируется система <<Электронное школьное расписание>>, в ней есть операция добавления нового класса (класс --- это имя и некая дополнительная информация); надо проверить, что имя класса еще не встречалось. Неудачный вариант спецификации этой проверки:
\begin{lstlisting}
check: Class-set >< ClassName >< ClassInfo -~-> Class-set
check(cset, cn, ci) is cset union {(cn,ci)}
pre (all c: Class :- c isin cset =>  let (cn2, ci2) = c in cn ~= cn2 )
\end{lstlisting}

Тут есть две проблемы:
\begin{enumerate}
    \item нечитабельные имена;
    \item длинная запись условия в предикате.
\end{enumerate}

Улучшенная версия:
\begin{lstlisting}
check: Class-set >< ClassName >< ClassInfo -~-> Class-set
check(classes, classname, classinfo) is
    classes union {(classname,classinfo)}
pre classname ~isin names(classes),

names: Class-set -> ClassName-set
names(classes) is
    { name(class) | class : Class :- class isin classes },

name: Class -> ClassName
name((classname,_)) is classname
\end{lstlisting}

Выбраны <<говорящие>> имена для параметров и добавлены 2 новые функции, с помощью которых предусловие стало возможным <<читать>>.

Еще пример для того же <<электронного расписания>>: пусть есть тип <<База данных>>, в нем несколько согласованных частей (одна хранит классы учащихся, другая учителей, третья аудитории); специфицируется функция, вносящая изменение в одну из частей (добавление нового класса учащихся). Неудачный вариант спецификации этой функции:
\begin{lstlisting}
add_class: DB >< Class -> DB
add_class(db, class) is
   let (classes, teachers, rooms, ....... ) = db in
        (classes union {class}, teachers, rooms, .... )
   end
\end{lstlisting}

текста получается много, взгляд разбегается, не знает, за что ухватиться, самое главное не высвечено.

Удачный вариант спецификации этой функции:
\begin{lstlisting}
add_class: DB >< Class -> DB
add_class(db, class) as db2
post
    classes(db2) = classes(db) union {class} /\
    teachers(db2) = teachers(db) /\
    rooms(db2) = rooms(db) /\ ....
\end{lstlisting}

Здесь постусловие (вместо явного задания) и выбор дополнительных <<говорящих>> функций позволяет выделить важное и кратко их записать.



\section*{Задачи}

\zhead{Написать неявную спецификацию следующих функций}

Обратите внимание на то, что следует описывать не алгоритм получения результата, а его свойства (<<наблюдаемые свойства>>).

\z Функция <<пересечения>> списков: возвращает список элементов, общих для каждого из двух данных списков.

\textbf{Решение:}

Заметьте, что это условие неполно, оно не говорит о том, в каком порядке должны быть элементы в результирующем списке, в каком количестве должны быть повторены элементы в результирующем списке (то, что они встречаются, например, по разу, совершенно не следует из постановки задачи). Поэтому написать спецификацию в явном виде не получится. Но несмотря на неполноту условия, сама функция осуществляет однозначное преобразование (но у нас пока что нет всей информации), любые два списка можно <<пересечь>>.

\begin{lstlisting}
value intsct: T-list >< T-list -> T-list
intsct(x, y) as z
post elems z = elems x inter elems y
\end{lstlisting}

\z Функция <<мультипликации списка>>: дан список t, дано натуральное число n; функция возвращает список, который состоит из n раз сконкатенированного списка t. Не описывайте алгоритм конкатенации, а пытайтесь выделить и записать полный набор свойств списка-результата.

\begin{lstlisting}
value ncopy: T-list >< Nat -> T-list
ncopy(t, n) as cp
post len cp = n * let t /\ (n > 0 => elems cp = elems t) /\
(all i:Nat :- i isin {1..n} =>
   t = <.cp(y + (i-1) * len t)|y in <.1..len t.>.>)
\end{lstlisting}

\z Функция получает множество элементов и возвращает список из них.

\textbf{Решение:}
\begin{lstlisting}
value set2list: T-set -> T-list
set2list(s) as l
post elems l = s
\end{lstlisting}

\z Функция получает множество элементов и возвращает список из них, каждый элемент должен встречаться ровно по одному разу.

\textbf{Решение:}
\begin{lstlisting}
value set2list: T-set -> T-list
set2list(s) as l
post elems l = s /\ len l = card s
\end{lstlisting}

\z Функция <<вычитания списков>>: даны два списка t1 и t2, функция строит список, являющийся копией t1, из которого удалены все элементы t2. Обратите внимание, что порядок и количество элементов из списка t1 (за исключением удаляемых) должен сохраниться в списке-результате.

\z Функция лексикографического сравнения двух списков: даны два списка t1 и t2 из целых чисел; функция возвращает отрицательное целое число, если список t1 лексикографически меньше списка t2, 0, если эти списки равны, положительное целое число, если список t1 лексикографически больше списка t2. Обратите внимание, что это неполное определение функции, но спецификация не может ничего добавлять <<от себя>> к этому определению!

\z Функция разделения на подсписки: дан список t и положительное целое число n; функция возвращает список списков, каждый список (за исключением. возможно, последнего) имеет длину n и конкатенация всех этих списков дает список t.

\z Функция удаляет первое вхождение заданного элемента в заданный список.

\z Функция удаляет последнее вхождение заданного элемента в заданный список.

\z Функция удаляет все вхождения заданного элемента в заданный список.

\z Функция возвращает первые n элементов заданного списка t, число n является натуральным.

\z Функция получает на вход список списков и возвращает список, составленный конкатенацией его элементов.

\z Функция получает на вход список и значение типа элемента этого списка, возвращает множество индексов вхождений этого элемента в список.

\z Функция получает на вход список и два значения типа элемента этого списка, функция производит замену всех вхождений первого значения на второе.

\z Функция получает на вход список строк и строку-разделитель, возвращает строку, составленную конкатенацией строк из списка через указанный разделитель.

\z Функция получает на вход список, возвращает реверсированную версию этого списка.

\z Функция получает на вход список и целое число, возвращает список, являющийся циклическим сдвигом данного списка на указанное количество шагов (положительное --- влево, отрицательное --- вправо, 0 --- без изменений).

\z Функция получает на вход множество натуральных чисел, возвращает список, в котором эти числа расположены по возрастанию. Обратите внимание, что количество повторов каждого элемента в списке может быть произвольным!

\z Функция получает на вход список натуральных чисел и сортирует его.

\z Функция получает на вход список и возвращает новый список, в котором каждый элемент исходного списка встречается ровно 1 раз.

\z Функция получает на вход список и возвращает новый список, в котором каждый элемент исходного списка встречается ровно 1 раз в том порядке, как они встретились в исходном списке.

\z Функция получает на вход 2 списка, в каждом списке элементы не повторяются, и возвращает их <<объединение>>: список, в котором все элементы обоих списков встречаются по разу.

\z Функция получает строку и возвращает множество всех ее подстрок.

\z Функция получает строку и возвращает ее подстроку. Внимание, требования на функцию неполные!

\z <<Задача о рюкзаке>>. Функция получается множество предметов: вес и стоимость каждого --- и вместимость рюкзака (максимальный вес вещей в нем). Функция возвращает множество предметов из данного множества, дающих максимум суммарной стоимости, умещающихся в рюкзаке.

\z Функция получает натуральное число и возвращает его факториал.

\textbf{Решение:}
\begin{lstlisting}
value f: Nat -> Nat
f(x) as y
post (exists n : Nat-list :- len n = x /\ hd n = 1 /\
(all i : Nat :- i < len n - 1 => n(i+2) = n(i+1)*(i+2)) /\ y = n(len n))
\end{lstlisting}

\z Функция получает на вход строку и два символа. Возвращает строку, в которой (по сравнению с данной) после каждого вхождения первого символа вставлен второй символ.

\z Функция получает на вход строку из круглых скобок. Функция возвращает true тогда и только тогда, когда эта строка является правильным скобочным выражением.

\z Функция получает на вход целое число и возвращает его строковое представление. Описывайте свойства этой строки, а не алгоритм ее получения!

\z Функция получает на вход строковое представление некоторого целого числа и возвращает это число.


\zhead{Задать модели типов и неявные спецификации функций}

% посмотреть живые примеры из http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/Jones1990.pdf
% Поиск в графах и задача о минимальном потоке: http://habrahabr.ru/blogs/algorithm/61884/

\z <<Система непересекающихся множеств (disjoint set union (DSU))>>. В этом задании надо сначала дать модель и спецификацию операций над системой непересекающихся множеств. Затем описать на RSL одну из эффективных реализаций этой структуры данных и операций. Обратите внимание на то, в каких случаях (для каких задач над программами) удобнее спецификация, нежели описание реализации.

Пускай мы оперируем элементами N видов (для простоты, здесь и далее — числами от 0 до N-1). Некоторые группы чисел объединены в множества. Также мы можем добавить в структуру новый элемент, он тем самым образует множество размера 1 из самого себя. И наконец, периодически некоторые два множества нам потребуется сливать в одно. Предложите модель для такой системы непересекающихся множеств и опишите для нее функциональность следующих операций:
\begin{itemize}
\item MakeSet(X) --- внести в структуру новый элемент X, создать для него множество размера 1 из самого себя;
\item Find(X) --- возвратить идентификатор множества, которому принадлежит элемент X. В качестве идентификатора мы будем выбирать один элемент из этого множества — представителя множества. Гарантируется, что для одного и того же множества представитель будет возвращаться один и тот же, иначе невозможно будет работать со структурой: не будет корректной даже проверка принадлежности двух элементов одному множеству if (Find(X) == Find(Y)).
\item Unite(X, Y) — объединить два множества, в которых лежат элементы X и Y, в одно новое.
\end{itemize}

Теперь на RSL реализуйте систему непересекающихся множеств так, как это предложили сделать Bernard Galler и Michael Fischer в 1964 году. Хранить структуру данных предлагается в виде леса, то есть превратить DSU в систему непересекающихся деревьев. Все элементы одного множества лежат в одном соответствующем дереве, представитель дерева — его корень, слияние множеств суть просто объединение двух деревьев в одно. Как мы увидим, такая идея вкупе с двумя небольшими эвристиками ведет к поразительно высокому быстродействию получившейся структуры.

Для начала потребуется массив p, хранящий для каждой вершины дерева её непосредственного предка (а для корня дерева X — его самого). С помощью одного только этого массива можно эффективно реализовать две первые операции DSU.

Чтобы создать новое дерево из элемента X, достаточно указать, что он является корнем собственного дерева, и предка не имеет.

\begin{lstlisting}
public void MakeSet(int x)
{
    p[x] = x;
}
\end{lstlisting}

Find(X) --- представителем дерева будем считать его корень. Тогда для нахождения этого представителя достаточно подняться вверх по родительским ссылкам до тех пор, пока не наткнемся на корень.

Но это еще не все: такая наивная реализация в случае вырожденного (вытянутого в линию) дерева может работать за O(N), что недопустимо. Можно было бы попытаться ускорить поиск. Например, хранить не только непосредственного предка, а большие таблицы логарифмического подъема вверх, но это требует много памяти. Или хранить вместо ссылки на предка ссылку на собственно корень — однако тогда при слиянии деревьев (Unite) придется менять эти ссылки всем элементам одного из деревьев, а это опять-таки временные затраты порядка O(N).

Вместо ускорения реализации будем просто пытаться не допускать чрезмерно длинных веток в дереве. Это первая эвристика DSU, она называется сжатие путей (path compression). Суть эвристики: после того, как представитель таки будет найден, для каждой вершины по пути от X к корню изменим предка на этого самого представителя. То есть фактически переподвесим все эти вершины вместо длинной ветви непосредственно к корню. Таким образом, реализация операции Find становится двухпроходной.

На рисунке показано дерево до и после выполнения операции Find(3). Красные ребра — те, по которым мы прошлись по пути к корню. Теперь они перенаправлены. Заметьте, как после этого кардинально уменьшилась высота дерева.

Исходный код операции Find в рекурсивной форме:

\begin{lstlisting}
public int Find(int x)
{
    if (p[x] == x) return x;
    return p[x] = Find(p[x]);
}
\end{lstlisting}

Unite(X, Y). Найдем для начала корни обоих сливаемых деревьев с помощью уже написанной функции Find. Теперь, помня, что наша реализация хранит только ссылки на непосредственных родителей, для слияния деревьев достаточно было бы просто подвесить один из корней (а с ним и все дерево) сыном к другому. Таким образом все элементы этого дерева автоматически станут принадлежать другому — и процедура поиска представителя будет возвращать корень нового дерева.

Встает вопрос: какое дерево к какому подвешивать? Всегда выбирать какое-то одно, скажем, дерево X, не годится: легко подобрать пример, на котором после N объединений мы получим вырожденное дерево — одну ветку из N элементов. И тут в ход вступает вторая эвристика DSU, направленная на уменьшение высоты деревьев.

Будем хранить помимо предков еще один массив Rank. В нем для каждого дерева будет храниться верхняя граница его высоты — то есть длиннейшей ветви в нем. Заметьте, не сама высота — в процессе выполнения Find длиннейшая ветвь может самоуничтожиться, а тратить еще итерации на нахождение новой длиннейшей ветви слишком дорого. Поэтому для каждого корня в массиве Rank будет записано число, гарантированно больше или равное высоте его дерева.

Теперь легко принять решении о слиянии: чтобы не допустить слишком длинных ветвей в DSU, будем подвешивать более низкое дерево к более высокому. Если их высоты равны — не играет роли, кого подвешивать к кому. Но в последнем случае новоиспеченному корню надо не забыть увеличить Rank.

\begin{lstlisting}
public void Unite(int x, int y)
{
    x = Find(x);
    y = Find(y);
    if (rank[x] < rank[y])
        p[x] = y;
    else
    {
        p[y] = x;
        if (rank[x] == rank[y])
            rank[x] = rank[x] + 1;
    }
}
\end{lstlisting}

Однако на практике оказывается, что можно и не тратить дополнительные O(N) памяти на ранги. Достаточно выбирать корень для переподвешивания случайным образом --- как ни удивительно, но такое решение дает на практике скорость, вполне сравнимую с оригинальной ранговой реализацией.

\z <<Декартово дерево>> (Treap) --- дерево, в вершинах которого хранятся пары ключей (x, y), причем
по первым компонентам пар (<<ключам>>) дерево является деревом поиска, а по вторым компонентам пар (<<приоритетам>>) --- кучей.

Реализуйте следующие операции Merge и Split над декартовыми деревьями. Операция Merge принимает на вход два декартовых дерева L и R. От нее требуется слить их в одно, тоже корректное, декартово дерево T. Следует заметить, что работать операция Merge может не с любыми парами деревьев, а только с теми, у которых все ключи одного дерева ( L ) не превышают ключей второго ( R ).

На вход операции Split поступает корректное декартово дерево T и некий ключ x0. Задача операции — разделить дерево на два так, чтобы в одном из них ( L ) оказались все элементы исходного дерева с ключами, меньшими x0, а в другом ( R ) — с большими. Никаких особых ограничений на дерево не накладывается.

Опишите сначала эти операции в неявном виде, не думая о том, как их реализовать (подумайте, как могла бы выглядеть алгебраическая спецификация --- оцените ее понятность и случаи, в которых она удобнее неявной спецификации). Готово? Теперь напишите такие их реализации на RSL.

\begin{lstlisting}
public static Treap Merge(Treap L, Treap R)
{
    if (L == null) return R;
    if (R == null) return L;

    if (L.y > R.y)
    {
        var newR = Merge(L.Right, R);
        return new Treap(L.x, L.y, L.Left, newR);
    }
    else
    {
        var newL = Merge(L, R.Left);
        return new Treap(R.x, R.y, newL, R.Right);
    }
}
\end{lstlisting}

\begin{lstlisting}
public void Split(int x, out Treap L, out Treap R)
{
    Treap newTree = null;
    if (this.x <= x)
    {
        if (Right == null)
            R = null;
        else
            Right.Split(x, out newTree, out R);
        L = new Treap(this.x, y, Left, newTree);
    }
    else
    {
        if (Left == null)
            L = null;
        else
            Left.Split(x, out L, out newTree);
        R = new Treap(this.x, y, newTree, Right);
    }
}
\end{lstlisting}


\zhead{По данной явной спецификации построить эквивалентную неявную спецификацию}

\z \begin{lstlisting}
variable lst: Int-list
value f: Unit -> write lst Int-list
  f() is local variable lst2:Int-list := <..> in
    for e in lst do
      if e ~isin elems lst2 then lst2 := lst2 ^ <.e.> end
    end; lst2  end
\end{lstlisting}

\textbf{Решение:} Функция возвращает список первых вхождений в обратном порядке. Идея записи постусловия: для каждого элемента списка-результата:
\begin{itemize}
    \item все предыдущие элементы не должны встречаться перед первым его вхождением;
    \item все последующие элементы должны встретиться перед первым его вхождением.
\end{itemize}

\begin{lstlisting}
variable lst: Int-list
value f: Unit -> write lst Int-list
f() as lst2
post lst = lst` /\
  let lst2 = card elems lst /\ elems lst2 = elems lst /\
  ( all i:Nat :- i isin inds lst2 =>
    ( exists j: Nat :- j isin inds lst /\ lst(j) = lst2(i) /\
               lst(j) ~isin { lst(k) | k:Nat :- k isin {1..j-1} } /\
       (all p:Nat :- p isin inds lst2 /\ p < i =>
         lst2(p) ~isin { lst(k) | k:Nat :- k isin {1..i-1} } ) /\
       (all p:Nat :- p isin inds lst2 /\ p > i =>
         lst2(p)  isin { lst(k) | k:Nat :- k isin {1..i-1} } ) ) )
\end{lstlisting}

\z \begin{lstlisting}
variable lst: Int-list
value f: Unit -> write lst Int-list
   f() is
    local variable lst2:Int-list := <..>, lst3: Int-list := lst in
    for e in lst do
        if lst3 ~= <..> then
           lst3 := tl lst3;
           if e ~isin elems lst3 then lst2 := lst2 ^ <.e.> end
       end
   end; lst2  end
\end{lstlisting}

\z \begin{lstlisting}
value f: Int-list -> Nat
  f(lst) is local variable m:Nat := 0,
         m2:Nat := 0, b:Bool := true in
    for i in <.1 .. len lst.> do
        m := 1; b := true;
        for j in <.i+1 .. len lst.> do
          if b /\ lst(j) >= lst(j-1)
            then m := m + 1
            else b := false end
          end;
          if m2 < m then m2 := m end
       end; m2 end
\end{lstlisting}

\z \begin{lstlisting}
value f: Nat-list -> Nat
  f(lst) is local variable lst2:Nat-list := lst,
             k:Nat := 0, m:Nat := 0 in
     for e in lst do
        if e > k then m := m + 1; k := e end;
    end; m end
\end{lstlisting}

\z \begin{lstlisting}
value f : Int >< Int -~-> write x,y,z Int >< Int >< Int
  f (a, b) is local variable v : Int := 0*1-y in
    for i in <.1+ a..b +2.> do if i > 3 then
      x := card ( {x,x+1,x,x-1}\{x*x} ) end;
      v := x + 2*(x:=v; x*i) end; (b+a, b-a, b-v) end
pre a>= b-10
\end{lstlisting}

\z \begin{lstlisting}
value f: Int >< Int >< Int -> write x,y,z Int >< Int >< Int >< Int
 f(a,b,c) is local variable v:Int:=c in
    y:=a; for t in <.a..b.> do
   if abs t < 3 /\ a ~=v then
      y := card dom ([2+>2]#[a+>x,v+>y]) end;
    v:= v+2*(x:=t;t)*(2+y)
  end;
  (a+b, x:=a-x;v, a+x, x:=a-x;a-b)
 end
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list -~-> Int >< Int
 f(lst) is local variable v: Int := hd lst,
           i: Int := 1, j: Int := 2 in
       for e in tl lst do
         if e > v then v := e; i := j end;
               j := j + 1
       end; (v, i) end
pre lst ~= <..>
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list -~-> Int >< Int
 f(lst) is local variable v: Int := hd lst,
           i: Int := 1, j: Int := 2 in
       for e in tl lst do
         if e >= v then v := e; i := j end;
               j := j + 1
       end; (v, i) end
pre lst ~= <..>
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list >< Int -~-> Int >< Int
 f(lst, x) is local variable i: Int := len lst,
           j: Int := len lst, s: Int := 0 in
     while j > 0 do
       if lst(j) = x then i := i - 1; s := j end;
            j := j - 1
      end; (i, s) end
 pre x isin elems lst
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list -~-> Int >< Int
   f(lst) is local variable v: Int := lst(len lst),
            i: Int := 1, j: Int := 1 in
       for e in <.len lst-i|i in <.1..len lst-1.>.>  do
          if lst(e) > v then v := lst(e); i := j end;
          j := j + 1
       end; (v, i) end
  pre lst ~= <..>
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list >< Int -~-> Int >< Int
  f(lst, x) is local variable i: Int := 0,
           j: Int := len lst, s: Int := 0 in
        while j > 0 do
           if lst(j) = x then i := i + 1; s := j end;
           j := j - 1
       end; (i, s) end
  pre x isin elems lst
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list -~-> Int >< Int
  f(lst) is local variable v: Int := hd lst,
        i: Int := 1, j: Int := 2 in
        for e in tl lst do
         if e < v then v := e; i := j end;
         j := j + 1
      end; (v, i) end
  pre lst ~= <..>
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list >< Int -~-> Int >< Int
  f(lst, x) is local variable i: Int := len lst,
     j: Int := 0, s: Int := 0 in
        for e in lst do
          if e = x then i := i - 1; s := j end;
          j := j + 1
       end; (i, s) end
  pre x isin elems lst
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list -~-> Int >< Int
   f(lst) is local variable v: Int := lst(len lst),
     i: Int := 1, j: Int := 1 in
    for e in <.len lst-i|i in <.1..len lst-1.>.>  do
      if lst(e) < v then v := lst(e); i := j end;
      j := j + 1
   end; (v, i) end
 pre lst ~= <..>
\end{lstlisting}

\z \begin{lstlisting}
value f : Int-list >< Int -~-> Int >< Int
  f(lst, x) is local variable i: Int := 0,
         j: Int := 0, s: Int := 0 in
       for e in lst do
         if e = x then i := i + 1; s := j end;
         j := j + 1
      end; (s, i) end
  pre x isin elems lst
\end{lstlisting}

\z \begin{lstlisting}
value f: Int-list >< Int -> Int
f(lst,x) is local variable i:Int := 0,
         j:Int := 1, k:Int := 0 in
   for e in lst do
      if e = x then
         k := k+1;
         if k = 2 then i := j end
      end;
      j := j + 1
    end;
    i
  end
\end{lstlisting}

\z \begin{lstlisting}
value f: Int-list >< Int -> Int
f(lst,x) is local variable i:Int := 0,
          j:Int := 1, k:Int := 0 in
     for e in lst do
         if e = x then i := k; k := j end;
         j := j + 1
     end;
     i
  end
\end{lstlisting}

\z \begin{lstlisting}
value f: Int-list >< Int -> Int
f(lst,x) is local variable i:Int := 0,
           j:Int := 1, k:Int := 0 in
     for e in <.len lst-i|i in <.0..len lst-1.>.> do
       if lst(e) = x then
           k := k+1;
           if k = 2 then i := j end
       end;
       j := j + 1
      end;
      i
end
\end{lstlisting}

\z \begin{lstlisting}
value f: Int-list -~-> Int >< Int
  f(lst) is local variable x:Int := len lst,
          y:Int := 1, m:Int := lst(x) in
     while y ~= x do
        local variable z: Int := 0 in
        if x\2 = abs (len lst \ 2 - y \ 2)
            then z := x + 1 else z := x - 1 end;
        if lst(y) < m then m := lst(y) end;
              x := y; y := z
     end
   end; (x,m)  end
  pre lst ~= <..>
\end{lstlisting}

\z \begin{lstlisting}
value f: Int-list -~-> Int >< Int
 f(lst) is local variable x:Int := 1,
        y:Int := len lst, m:Int := hd lst in
     while y ~= x do
         local variable z: Int := 0 in
         if x\2 = abs (len lst \ 2 - y\2)
          then z := x - 1 else z := x + 1 end;
         if lst(y) > m then m := lst(y) end;
         x := y; y := z
     end
   end; (x,m)  end
 pre lst ~= <..>
\end{lstlisting}


%%%%%%%%%%%%%%%%%%\zhead{По данной алгебраической спецификации предложить модели типов и явные или неявные определения функций}
%Выделить наислабейшие предусловия для функций.
%
%% спецификация функций стандартной библиотеки Си: http://www.open-std.org/JTC1/SC22/wg14/www/docs/n1124.pdf
%
%% спецификация протоколов (формат сообщений и правила преобразования сообщений)
%
%% описание недетерминированности в детерминированных предусловиях (разное поведение, мы еще не выбрали из них окончательное)
%% --- как в играх ("крестики-нолики")
%
%


\zhead{Выделить и формализовать программные контракты функций и инварианты на данные}

\z <<Шашки>>. Задача системы --- визуализировать поле игры (Square) и модифицировать его в ответ на команды игрока. Поле 8 на 8. У каждого игрока 12 шашек. Отличия от стандартных шашек:
\begin{enumerate}
  \item бить назад нельзя;
  \item бить несколько шашек нельзя;
  \item если шашка должна стать <<дамкой>>, она в <<дамку>> не превращается;
  \item игра заканчивается, если никакой дальнейший ход невозможен или на доске остались шашки только одного цвета (выигрывает тот, у кого осталось больше шашек; ничья, если их количество одинаковое).
\end{enumerate}
\begin{lstlisting}
type	Color = Bool,
	Nat8 = {| n : Nat :- n isin {1..8} |},
	Coord = Nat8 >< Nat8,
	Source = Coord, Destination = Coord,
	Square = Coord -m-> Color,
value
	move : Square >< Source >< Destination -~-> Square,
	newgame : Unit -> Square
\end{lstlisting}


\z <<Неазартное 21>> Задача системы --- визуализировать поле игры (Game) и модифицировать его в ответ на команды игрока. В колоде 36 карт (вальты, дамы, короли, тузы, 6-ки, 7-ки, 8-ки, 9-ки и 10-ки четырех мастей); стоимость карт: валет -- 2, дама -- 3, король -- 4, туз -- 11, 6-ки-10-ки имеют стоимость, соответствующую своему названию. Банкир (Banker) играет с единственным игроком-соперником (Gambler). Сначала игрок берет из колоды (PackOfCards) себе карты (набирает свой Hand), затем банкир берет из колоды себе карты. Если сумма набранных баллов по картам у игрока равна 21, он выиграл; больше 21 - проиграл; иначе если у банкира 21, он выиграл; если больше 21 - проиграл; в противном случае выигрывает тот, кто набрал большую сумму баллов.

\begin{lstlisting}
type Token, Card = Token -m-> {| n : Nat :- n isin {2..11}\{5} |},
     Hand = Card-set, Banker = Hand, Gambler = Hand,
     PackOfCards = Card-list, Game = Gambler >< PackOfCards >< Banker,
value newgame : Unit -~-> Game,
  gamblerMove : Game >< Bool -~-> Game,
  bankerMove : Game >< Bool -~-> Game
\end{lstlisting}

newgame : если карта берется, то в случае gamblerMove она переносится из PackOfCards в Gambler, в случае bankerMove - в Banker;

gamblerMove : 2-й аргумент --- прекращение выбора карт;

bankerMove : 2-й аргумент --- прекращение выбора карт.


\z <<Домино>> Задача системы --- визуализировать поле игры (Game) и модифицировать его в ответ на команды игрока. Играют двое. Вначале каждый игрок произвольным образом получает половину всех доминошек (14 штук). Ход игрока (move) заключается в выборе доминошки из своей кучи (Hand) и вставки его линию (Line) с подходящего конца (если подходит к обоим концам, игрок выбирает сам, на какой конец он ставит доминошку). Если игроку нечем походить, он проигрывает.

\begin{lstlisting}
type Token = {| n : Nat :- n <= 6 |} >< {| n : Nat :- n <= 6 |},
  Hand = Token-set, Line = Token-list,
  Game = Hand >< Hand >< Line
value
  move : Game >< Token -~-> Game,
  newgame : Unit -~-> Game
\end{lstlisting}

move: <<ход игрока>>, либо одного, либо другого.

\z <<Пятнашки>> Задача системы --- визуализировать поле игры (Square) и модифицировать его в ответ на команды игрока (move). Поле 4 на 4 клетки. Общее число фишек 15 (все пронумерованы от 1 до 15). Ход игрока состоит в том, что нужно передвинуть одну из фишек, соседствующих с пустой клеткой (Nat4 >< Nat4) на пустое место. Цель игры - выстроить фишки в соответствии с их номерами. Начальное состояние - случайное (newgame).

\begin{lstlisting}
type 	Nat4 = {| n : Nat :- n isin {1..4}  |},
	Nat15 = {| n : Nat :- n isin {1..15} |},
	Square = Nat4 >< Nat4 -m-> Nat15
value
	move : Square >< Nat4 >< Nat4 -~-> Square,
	newgame : Unit -~-> Square
\end{lstlisting}

\z <<Кофе-автомат>> (coffee-machine). Задача системы - управлять интерфейсом автомата, который состоит из индикаторов <<готов>> и <<жду монету>>, устройства ввода монеты, кнопки <<возврат денег>>, устройства выдачи чашки с кофе, устройства возврата монет. Индикатор <<готов>> горит, когда в автомате есть вода и сухой кофе (эти ресурсы могут исчерпаться после продолжительного использования), индикатор <<жду монету>> загорается после ввода первой монеты и гаснет после того, как сумма введенных монет в точности равняется цене чашки кофе. Монета отбраковывается (это единственная причина), если сумма уже введенных монет с этой превысит цену чашки кофе.

Действие функции proceed. Функция вызывается каждый раз, когда клиент вводит очередную монету. Результатом функции является корректировка параметров <<объем воды>> и <<вес кофе>> (если кофе наливается), новое значение состояния индикаторов, включение (или невключение --- значение параметра типа CoinDischarge равно 0) устройства возврата монет (значение параметра типа CoinDischarge равно 1 - вернуть одну, последнюю, монету).

Действие функции flush. Функция вызывается кнопкой <<возврат денег>>. Функция выдает новое состояние индикаторов и параметр - число возвращаемых монет, равное числу введенных клиентом монет.

Требуется определить ограничения на типы данных и на значения констант и пред- и пост-условия функций.

\begin{lstlisting}
type	ReadyIndicator = Bool, CoinExpectIndicator = Bool,
	WaterVolume = Real, CoffeeWeight = Real,
    Coin = Nat, CoinDischarge = Nat,
	CoffeeMachine = (WaterVolume >< CoffeeWeight >< Coin-list)
value
  waterPortion : Real,
  coffeePortion : Real,
  cupPrice : Nat,
  proceed : CoffeeMachine >< Coin -> CoffeeMachine ><
	   ReadyIndicator >< CoinExpectIndicator
     >< CoinDischarge,
  flush : CoffeeMachine -> CoffeeMachine >< ReadyIndicator
        >< CoinExpectIndicator >< CoinDischarge
\end{lstlisting}

\z <<Попкорн-автомат>> (popcorn-machine). Задача системы - управлять интерфейсом автомата, который состоит из индикаторов <<введите купюру>> и <<выберите сорт>>, меню <<вид попкорна>>, кнопки <<возврат денег>>, устройства выдачи стаканчика с попкорном, устройства возврата купюры. Индикатор <<введите купюру>>  горит, когда в автомате есть стаканы и кукуруза (эти ресурсы могут исчерпаться после продолжительного использования). Индикатор <<выберите сорт>> загорается после ввода купюры и гаснет после выдачи кукурузы или возврата купюры. Если попкорн требуемого вид закончился, то ничего не происходит.

Функция money. Функция вызывается каждый раз, когда клиент вводит купюру.

Функция menu\_push. Функция вызывается при нажатии пункта меню на автомате. Если данный вид попкорна есть, то выдается стаканчик с попкорном, происходит корректировка параметров <<объем попкорна>> данного вида (PopCorn) и <<число стаканов>> (CupNumber), новое значение состояния индикаторов, включение (или невключение) устройства выдачи стаканчика с попкорном.

Функции flush. Функция вызывается кнопкой <<возврат денег>>. Функция выдает новое состояние индикаторов и включает устройство возврата купюры (побочный эффект, который не специфицируется).
Величины в rng типа данных PopCornPrice --- это цена одной единицы объема соответствующего вида. Данные типа PopCorn указывают остаток каждого вида попкорна в бункерах.

Требуется определить ограничения на типы данных и на значения констант и пред- и пост-условия функций.

\begin{lstlisting}
type	InputBanknote = Bool, ChooseKind = Bool,
    CupVolume = Real, Rubles = Nat,
	Kind, CupNumber = Nat, Banknotes = Rubles,
    PopCorn = Kind-m->Real, PopCornPrice = Kind-m->Rubles,
    PopCornMachine = (CupNumber >< PopCorn >< Banknotes)
value
	price : PopCornPrice, 	
	money : PopCornMachine >< Rubles ->
             PopCornMachine >< InputBanknote >< ChooseKind,
	menu_push: PopCornMachine >< Kind ->
             PopCornMachine >< InputBanknote >< ChooseKind,
	flush : PopCornMachine ->
             PopCornMachine >< InputBanknote >< ChooseKind
\end{lstlisting}

\z <<Разменный автомат>> Задача системы --- управлять интерфейсом автомата, который состоит из индикаторов <<готов>> и <<принятая сумма>>, меню <<максимальный номинал>>, кнопки <<возврат денег>>, устройства выдачи денег. Индикатор <<готов>> горит, когда в автомате есть деньги для размена принятой суммы (этот ресурс может исчерпаться после продолжительного использования). Индикатор <<принятая сумма>> показывает сумму номиналов купюр, введенных клиентом. После нажатия кнопки <<возврат денег>> или после удачного выбора меню этот индикатор показывает <<0>>. В любой момент клиент может выбрать в меню максимальный номинал для размена. Если набор имеющихся банкнот в автомате позволяет это сделать, автомат производит размен через устройство выдачи денег, если походящего набора нет, то ничего не происходит.

Функция money. Функция вызывается каждый раз, когда клиент вводит купюру.

Функция menu\_push. Функция вызывается при нажатии некоторой позиции в меню на аппарате. Если размен возможен,  то результат типа Action=true (включается устройство выдачи денег), корректируются показатели индикаторов, корректируется модель Cashier. Если размен невозможен, то ничего не происходит, Action=false.

Функция flush. Функция вызывается кнопкой <<возврат денег>>. Функция выдает новое состояние индикаторов и включает устройство выдачи денег (побочный эффект, который не специфицируется).

Требуется определить ограничения на типы данных и пред- и пост-условия функций.

\begin{lstlisting}
type	ReadyIndicator = Bool, SumIndicator = Nat,
	Nominal = Nat, Menu = Nominal-list,
	Bank = Nominal -m-> Nat, ClientInput = Nat,
	Cashier = (Bank >< ClientInput), Action = Bool
value
  menuNominals : Menu := <.10, 50, 100, 500, 1000, 5000.>,
  money : Cashier >< Nominal -~->
     Cashier >< ReadyIndicator >< SumIndicator,
  menu_push : Cashier >< Nominal -~->
     Cashier >< ReadyIndicator >< SumIndicator >< Action,
  flush : Cashier -> Cashier >< ReadyIndicator >< SumIndicator
\end{lstlisting}

\z Модель игры <<Эскалатор>>. Простая видео-игра. На экране изображен эскалатор метро и пассажиры. Эскалатор (на экране) движется с постоянной скоростью вверх-налево (1 ступень в 1 квант времени). Пассажиры спонтанно появляются на площадке перед входом на эскалатор. Система сама следит, чтобы на площадке было не более 2-х пассажиров. При выходе с эскалатора пассажиры оказываются на противоположной площадке и тут же исчезают из поля зрения.

Пользователь может кликнуть по пассажиру левой или правой кнопкой <<мыши>>. Клик левой кнопкой означает <<шаг вперед>> (войти на эскалатор или подняться на 1 ступень); клик правой --- <<шаг назад>> или вернуться с первой степени эскалатора на площадку. Программная модель следит, чтобы на одной ступени эскалатора находилось не более двух пассажиров и на обеих площадках находилось не более двух пассажиров. Пользователь может кликнуть мышкой на любом из пассажиров в любой момент времени и, если передвижение пассажира может нарушить это правило <<не более 2-х пассажиров>>, то действие клика игнорируется.	

Функция forward. Функция вызывается каждый раз, когда пользователь кликает левой кнопкой <<мышки>> на соответствующем пассажире.

Функция back. Функция вызывается каждый раз, когда пользователь кликает правой кнопкой <<мышки>> на соответствующем пассажире.

Функция tick. Функция вызывается каждый раз, когда истекает очередной квант времени, ее действие состоит в продвижении эскалатора на ступеньку. Если при этом на верхней ступеньке еще находится пассажир, он переносится на верхнюю площадку принудительно.

Величины First и Last указывают на начало о конец видимой части эскалатора и, соответственно, увеличиваются по модулю общего числа ступенек эскалатора по истечении каждого кванта времени.

Требуется определить ограничения на типы данных и пред- и пост-условия функций.

\begin{lstlisting}
type	Passenger = Nat, First = Nat, Last = Nat,
	Steir = Passenger-set, Bottom = Passenger-set,
    Top = Passenger-set,
	Escalator = (Bottom >< Steir-list >< First >< Last >< Top)
value
	tick : Escalator -> Escalator,
	forward : Escalator >< Passenger -> Escalator,
	back : Escalator >< Passenger -> Escalator
\end{lstlisting}




\zhead{Уточнение спецификаций}

В каждой следующей задаче дана последовательность заданий одних и те же функций, но последующие задания уточняют предыдущие. Формализуйте каждое такое задание и покажите, имеет ли место уточнение.

\z <<Кэш-1>>

Спецификация №1: кэш представляет собой хранилище данных, снабженных тегами, т.е. данные добавляются в кэш вместе с тегом.

Спецификация №2: кэш представляет собой хранилище данных, снабженных тегами, т.е. данные добавляются в кэш вместе с тегом. При переполнении удаляется одна порция данных.

\textbf{Решение:}

В учебных целях сначала будет показано неверное решение этой задачи. А именно, первая спецификация формализуется следующим образом:
\begin{lstlisting}
scheme Cache_1 = class
  type Tag, Data, Cache = Tag -m-> Data
  value add: Cache >< Tag >< Data -> Cache
        add(cache, tag, data) is
             cache !! [tag +> data]
end
\end{lstlisting}

Вторая спецификация формализуется следующим образом:
\begin{lstlisting}
scheme Cache_2 = class
  type Tag, Data, Cache = Tag -m-> Data
  value size : Nat
  value add: Cache >< Tag >< Data -> Cache
    add(cache1, tag, data) as cache2
    post
      if card dom cache1 < size then
        cache2 = cache1 !! [tag +> data]
      else
       card dom cache1 = size /\
       card dom cache2 = size /\
       tag isin dom cache1 /\
       cache1(tag) = data /\
       (tag ~isin dom cache1 =>
           card (dom cache1 \ dom cache2) = 2 /\
           (all t : Tag :- (t isin dom cache2 /\ t ~= tag) =>
               (t isin dom cache1 /\ cache1(t) = cache2(t) )))
      end
end
\end{lstlisting}

Очевидно, что при данной формализации вторая спецификация \textbf{не является уточнением} первой спцификации. Однако у адекватного читателя такой результат должен вызвать подозрение. И оно обосновано: данная формализация первой спецификации предполагает, что все данные, которые были до добавления, остались в кэше (с другими тегами). Но это совершенно не следует из неформального описания первой спецификации! Слово <<добавляются данные>> не предусматривает, что при этом ничего не удаляется! Этот пример первой спецификации в неформальном виде демонстрирует неоднозначность естественного языка. Поэтому правильной будет следующая спецификация:
\begin{lstlisting}
scheme Cache_1 = class
  type Tag, Data, Cache = Tag -m-> Data
  value add: Cache >< Tag >< Data -> Cache
        add(cache1, tag, data) as cache2
        post tag isin dom cache2 /\ cache2(tag) = data
end
\end{lstlisting}

Теперь очевидно, что на каждой ветке постусловия во второй спецификации выполнено постусловие в первой спецификации, из чего следует наличие уточнения. Формальное доказательство этого факта предоставляется читателю.

По большому счёту предложенная модель данных тоже вызывает подозрения, поскольку нигде в требованиях не сказано, что не может быть разных данных с одинаковыми тегами.


\z <<Кэш-2>>

Спецификация №1: кэш представляет собой хранилище данных, снабженных тегами. По тегу можно получать данные.

Спецификация №2: кэш представляет собой хранилище данных, снабженных тегами. По тегу можно получать данные. Если таких данных нет, то в кэш помещаются некие данные по запрошенному тегу. Если кэш переполняется, одна из порций данных оттуда удаляется.

Спецификация №3: кэш представляет собой хранилище данных, снабженных тегами. По тегу можно получать данные. Если таких данных нет, то в кэш помещаются некие данные по запрошенному тегу. Каждая порция данных снабжена временем, жизни данных в кэше. При переполнении удаляются данные с максимальным временем жизни в кэше.

\textit{Примечание:} подумайте над замкнутостью набора операций !!!

Спецификация №4: кэш представляет собой хранилище данных, снабженных тегами. По тегу можно получать данные. Если таких данных нет, то в кэш помещаются некие данные по запрошенному тегу. Каждая порция данных снабжена временем, жизни данных в кэше. Если к порции данных происходит обращение, время обнуляется. При переполнении удаляются данные с максимальным временем жизни в кэше.


\zhead{Уточнить данную алгебраическую спецификацию до модельной спецификации}

\z \begin{lstlisting}
type E, T
value empty: T,
  add: T >< E -> T,
  include: T >< E -> Bool
axiom forall e, e1 : E, t : T :-
  ~include(empty, e),
  include(add(t, e), e),
  include(add(t, e), e1) is include(t,e1) pre e ~= e1
\end{lstlisting}

\textbf{Решение:}

Из этой спецификации следует, что isin даст false, если ему передан empty или если ему передан элемент, с которым до этого не вызывался add. При этом <<состояние специфицируемого компонента>> (т.е. значение типа Т) должно хранить в себе все элементы, с которыми ранее был вызван add, иначе невозможно будет однозначно описать функцию include.

\begin{lstlisting}
type E, T = E-set
value empty: T = {},
  add: T >< E -> T
  add(t,e) is t union {e},
  include: T >< E -> Bool
  include(t,e) is e isin t
\end{lstlisting}

Формальное доказательство того, что эта спецификация уточняет данную алгебраическую предоставляется читателю.

Уточнение можно сделать и иначе, главное, сохранить свойство <<насыщения>> операции add:
\begin{lstlisting}
type E, T = E-list
value empty: T = <..>,
  add: T >< E -> T
  add(t,e) is <.e.> ^ t,
  include: T >< E -> Bool
  include(t,e) is e isin elems t
\end{lstlisting}

\z \begin{lstlisting}
type E, T
value empty: T,
  add: T >< E -> T,
  count: T >< E -> Nat
axiom forall e, e1 : E, t : T :-
  count(empty, e) is 0,
  count(add(t, e), e) is count(t, e) + 1,
  count(add(t, e), e1) is count(t,e1) pre e ~= e1
\end{lstlisting}


\z \begin{lstlisting}[escapechar={|}]
type E, S
value capacity: Nat,
    empty: Unit -~-> S,
    |is\_empty|: S -> Bool,
    push: S >< E -~-> S,
    pop: S -~-> S >< E,
    top: S -> Nat,
    elem: S >< Nat -~-> E,
    f: S >< E -> S f(s,e) is s,
    sc: S >< E -> S sc(s,e) is e
axiom forall s: S, e: E, i: Nat :-
  top( empty() ) is 0,
  top( push(s, e) ) is top(s) + 1 pre top(s) < capacity,
  top( pop(s, e) ) is top(s) - 1 pre ~|is\_empty|(s),
  elem( push(s, e), top(s) + 1 ) is e pre top(s) < capacity,
  elem( push(s,e), i ) is elem(s, i)
        pre i ~= top(s) + 1 /\ top(s) < capacity,
  elem( f(pop(s)), i ) is elem(s, i) pre i ~= top(s),
  elem( s, top(s) ) is sc(pop(s))  pre ~|is\_empty|(s),
  |is\_empty|( empty() ),
  ~|is\_empty|( push(s,e) ),
  capacity > 0
\end{lstlisting}

\z \begin{lstlisting}
type Owner, Auto, Warrant
value
    empty: DB,
    add: Owner >< DB -~-> DB,
    known: Owner >< DB -> Bool,
    known: Auto >< DB -> Bool,
    known: Warrant >< DB -> Bool,
    add: Owner >< Auto >< DB -~-> DB,
    add: Auto >< Warrant >< DB -~-> DB,
    get_owner: Auto >< DB -~-> Owner
axiom forall o1, o2 : Owner,
    a, a2 : Auto, db : DB, w, w2 : Warrant :-
    ~ known(o1, empty),
    known(o1, add(o2, db)) is o1 = o2 \/ known(o1, db)
            pre ~known(o2, db),
    known(o1, add(o2,a,db)) is known(o1,db)
            pre known(o2,db) /\ ~known(a,db),
    known(o1, add(a,w,db)) is known(o1,db)
            pre known(a,db) /\ ~known(w,db),

    ~ known(a, empty),
    known(a, add(o1,db)) is known(a,db)
        pre ~known(o1,db),
    known(a, add(o2,a2,db)) is a = a2 \/ known(a,db)
        pre known(o2,db) /\ ~known(a2,db),
    known(a, add(a2,w,db)) is known(a,db)
        pre known(a2,db) /\ ~known(w,db),

    ~known(w, empty),
    known(w, add(o, db)) is known(w, db)
        pre ~known(o, db),
    known(w, add(a,w2, db)) is w = w2 \/ known(w,db)
        pre known(a,db) /\ ~known(w2,db),
    known(w, add(o, a, db)) is known(w,db)
        pre known(o, db) /\ ~known(a,db),

    get_owner(a, add(o,db)) is get_owner(a, db)
        pre ~known(o, db) /\ known(a, db),
    get_owner(a, add(o, a2, db)) is if a = a2 then o
        else get_owner(a, db) end
        pre known(o,db) /\ ~known(a2, db) /\
            (a = a2 \/ known(a,db)),
    get_owner(a, add(a2,w,db)) is get_owner(a,db)
        pre known(a2,db) /\ ~known(w,db) /\
            known(a,db)
\end{lstlisting}




%\chapter{Применение формальных спецификаций}

%\section{?????}
%
%Формальные спецификации позволяют не только заведома выявить скрытые и недоопределенные места в требованиях, но и автоматизировать деятельность по оценке корректности реализации системы (верификация, автоматическая генерация тестов, оценка качества (покрытия) тестов, полученных разными способами).
%
%Для формализации различных требований подходят и разные стили спецификации, одни из них ближе к формулировке требований от заказчика, другие ближе к формулировке требований на программный код для инженера-программиста.
%
%При работе с задачами помните, что речь всегда идет об интерфейсах программных компонентов, о <<ядре>> программной системы (а не, например, о визуальном интерфейсе).
%
%\section*{Задачи}
%
%\zhead{???????????}
%
%В каждой задаче описана разрабатываемая программная система. Требуется составить требования в том виде (в том стиле), как они сформулированы в задаче, проанализировать их на согласованность и полноту, при необходимости уточнить естественным образом, подчёркивая те моменты, которые пришлось уточнять, затем составить программные контракты для функций программной системы.
%
%\z \emph{Система файлового хранения}. Есть пользователи, которые размещают файлы в системе. У каждого пользователя есть счёт. Файл можно скачать за одну цену с одной скоростью и с другой, меньшей, ценой на меньшей скорости. При этом при скачивании пользователю, который этот файл разместил в системе, идет некоторый процент цены. Часть цены идёт самой системе. Пользователи могут регистрироваться в системе по приглашениям других пользователей. Если <<друг>> пользователя скачивает файл, часть цены за файл идет на счёт этого пользователя.
%
%\textit{Замечание:} обратите внимание, что требования вида <<при таком-то действии в системе изменяются некие характеристики ее компонент>> имеют алгебраическую природу.

\section{Аналитическая верификация: методы Флойда}

\section*{Задачи}

Во всех задачах $x_1, x_2, ...$ --- входные переменные, $y_1, y_2, ...$ --- промежуточные переменные, $z_1, z_2, ...$ --- выходные переменные. Если не сказано противное, входные переменные обладают целыми неотрицательными значениями.

Если в алгоритмах не указано условие у оператора цикла, значит это условие --- тождественная истина (т.е. цикл бесконечный).

\zhead{Доказать частичную корректность следующих числовых алгоритмов\footnote{Часть задач взяты из~\cite{Shen}, часть задач составлены Алексеем Хорошиловым}}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = x_1 \cdot x_2)$

\begin{codebox}
\Procname{$\proc{Multiply}(x_1,x_2)$}
\li $y_1 \gets 0$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_2$
\li \Do $(y_1,~y_2) \gets (y_2 + x_1,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1)~is~true$, $post(x_1, z)~is~(z = x_1 \cdot (x_1 + 1))$

\begin{codebox}
\Procname{$\proc{Arithmetic}(x_1)$}
\li $y_1 \gets 0$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_1$
\li \Do $(y_1,~y_2) \gets (y_1 + 2y_2,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1)~is~true$, $post(x_1, z)~is~(z = x_1 \cdot (x_1 + 1) \cdot (2x_1 + 1))$

\begin{codebox}
\Procname{$\proc{SumSquare}(x_1)$}
\li $y_1 \gets 0$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_1$
\li \Do $(y_1,~y_2) \gets (y_1 + 6y_2\cdot y_2,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = x_1^{x_2})$

\begin{codebox}
\Procname{$\proc{Power}(x_1,x_2)$}
\li $y_1 \gets 1$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_2$
\li \Do $(y_1,~y_2) \gets (y_1 * x_1,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~(x_2 > 0)$, $post(x_1, x_2, z)~is~(z = x_1^{x_2})$

\begin{codebox}
\Procname{$\proc{Power}(x_1,x_2)$}
\li $y_1 \gets x_1$
\li $y_2 \gets 1$
\li \While $y_2 < x_2$
\li \Do \If $2y_2 \leq x_2$
\li \Then $(y_1,~y_2) \gets (y_1 * y_1,~2y_2)$
\li \Else $(y_1,~y_2) \gets (y_1 * x_1,~y_2 + 1)$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = x_1^{x_2})$

\begin{codebox}
\Procname{$\proc{Power}(x_1,x_2)$}
\li $y_1 \gets 1$
\li $y_2 \gets 0$
\li \While $y_2 < x_2$
\li \Do \If $y_2 = 0$
\li \Then $(y_1,~y_2) \gets (x_1,~1)$
\li \Else \If $2y_2 \leq x_2$
\li \Then $(y_1,~y_2) \gets (y_1 * y_1,~2y_2)$
\li \Else $(y_1,~y_2) \gets (y_1 * x_1,~y_2 + 1)$ \End \End \End
\li $z \gets y_1$
\end{codebox}

% НОД
\z (<<GCD>> -- greatest common divisor) $pre(x_1, x_2)~is~(x_1 + x_2 > 0)$, $post(x_1, x_2, z)~is~(z = \gcd(x_1,x_2))$

\begin{codebox}
\Procname{$\proc{GCD}(x_1,x_2)$}
\li \If $x_1 > x_2$
\li \Then $y_1 \gets x_1$
\li \Else $y_1 \gets x_2$ \End
\li \While $x_1 \mod y_1 \neq 0 ~\vee~ x_2 \mod y_1 \neq 0$
\li \Do $y_1 \gets y_1 - 1$ \End
\li $z \gets y_1$
\end{codebox}

\z (<<GCD>> -- greatest common divisor) $pre(x_1, x_2)~is~(x_1 + x_2 > 0)$, $post(x_1, x_2, z)~is~(z = \gcd(x_1,x_2))$

\begin{codebox}
\Procname{$\proc{GCD}(x_1,x_2)$}
\li $y_1 \gets x_1$
\li $y_2 \gets x_2$
\li \While $y_1 > 0 ~\wedge~ y_2 > 0$
\li \Do \If $y_1 \geq y_2$
\li     \Then $y_1 \gets y_1 - y_2$
\li     \Else $y_2 \gets y_2 - y_1$ \End \End
\li \If $y_1 = 0$
\li \Then $z \gets y_2$
\li \Else $z \gets y_1$ \End
\end{codebox}

\z (<<LCM>> -- least common multiple) $pre(x_1, x_2)~is~(x_1 + x_2 > 0)$, $post(x_1, x_2, z)~is~(z = 2\cdot \mbox{lcm}(x_1,x_2))$

\begin{codebox}
\Procname{$\proc{2LCM}(x_1,~x_2)$}
\li $(y_1,~y_2,~y_3,~y_4) \gets (x_1,~x_2,~x_2,~x_1)$
\li \While $y_1 \neq 0 ~\wedge~ y_2 \neq 0$
\li \Do \If $y_1 \geq y_2$
\li     \Then $(y_1,~y_4) \gets (y_1 - y_2,~y_3 + y_4)$
\li     \Else $(y_2,~y_3) \gets (y_2 - y_1,~y_3 + y_4)$ \End \End
\li \If $y_1 = 0$
\li \Then $z \gets y_4$
\li \Else $z \gets y_3$ \End
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z = x^2)$

\begin{codebox}
\Procname{$\proc{Square}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~0)$
\li \While $y_1 < x$
\li \Do $(y_1,~y_2,~y_3) \gets (y_1 + 1,~y_2 + 2,~y_2 + y_3)$ \End
\li $z \gets y_1 + y_3$
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z^2 \leq x < (z+1)^2)$

\begin{codebox}
\Procname{$\proc{Sqrt}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~1)$
\li \While
\li \Do $y_2 \gets y_2 + y_3$
\li \If $y_2 > x$
\li \Then break
\li \Else $(y_1,~y_3) \gets (y_1 + 1,~y_3 + 2)$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~(x_1 > 0)~\wedge~(x_2 > 0)$, $post(x_1, x_2, z_1, z_2)~is~(0 \leq z_2 < x_2)~\wedge~(x_1 = z_1 \cdot x_2 + z_2)$

\begin{codebox}
\Procname{$\proc{Division}(x_1, x_2)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~x_1)$
\li \While $y_3 \neq 0$
\li \Do $y_1 \gets if~(y_2 + 1 = x_2)~then~(y_1 + 1)~else~y_1$
\li     $y_2 \gets if~(y_2 + 1 = x_2)~then~0~else~(y_2 + 1)$
\li     $y_3 \gets y_3 - 1$ \End
\li $(z_1,~z_2) \gets (y_1,~y_2)$
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z = x^2)$

\begin{codebox}
\Procname{$\proc{Square}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~1,~1-x)$
\li \While $y_3 < x$
\li \Do \If $odd(y_2)$
\li     \Then $y_1 \gets y_1 + y_2$ \End
\li     $(y_2,~y_3) \gets (y_2 + 1,~y_3 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

$odd(x)$ истинно тогда и только тогда, когда $x$ нечетно.

\z $pre(x)~is~true$, $post(x, z)~is~(z^3 \leq x < (z+1)^3)$

\begin{codebox}
\Procname{$\proc{Cubert}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~1)$
\li \While
\li \Do $y_2 \gets y_2 + y_3$
\li     \If $y_2 > x$
\li     \Then break
\li     \Else $y_1 \gets y_1 + 1$
\li             $y_3 \gets y_3 + 6y_1$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x)~is~(x < 102)$, $post(x, z)~is~(z = 91)$

\begin{codebox}
\Procname{$\proc{Century}(x)$}
\li $(y_1,~y_2) \gets (x,~1)$
\li \While $y_1 < 101 ~\vee~ y_2 \neq 1$
\li \Do \If $y_1 > 100$
\li     \Then $(y_1,~y_2) \gets (y_1 - 10,~y_2 - 1)$
\li     \Else $(y_1,~y_2) \gets (y_1 + 11,~y_2 + 1)$ \End \End
\li $z \gets y_1 - 10$
\end{codebox}

\z $pre(x)~is~(x > 1)$, $post(x, z)~is~(z = x^3)$

\begin{codebox}
\Procname{$\proc{Qube}(x)$}
\li $(y_1,~y_2,~y_3) \gets (x,~1,~x)$
\li \While
\li \Do \If $y_2 < y_3$
\li     \Then $(y_1,~y_2) \gets (y_1 + x,~y_2 + 1)$
\li     \Else \If $y_3 = x$
\li         \Then $y_3 \gets y_1$
\li         \Else break \End \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z = x^2)$

\begin{codebox}
\Procname{$\proc{Square}(x)$}
\li $(y_1,~y_2) \gets (x,~1)$
\li \While $y_2 < x$
\li \Do \If $2y_2 \leq x$
\li     \Then $(y_1,~y_2) \gets (2y_1,~2y_2)$
\li     \Else $(y_1,~y_2) \gets (y_1 + x,~y_2 + 1)$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = {x_1}^{x_2})$ ($0^0~is~1$)

\begin{codebox}
\Procname{$\proc{Power}(x)$}
\li $(y_1,~y_2,~y_3) \gets (x_1,~x_2,~1)$
\li \While $y_2 \neq 0$
\li \Do \If $odd(y_2)$
\li     \Then $(y_2,~y_3) \gets (y_2 - 1,~y_1 \cdot y_3)$
\li     \Else $(y_1,~y_2) \gets (y_1 \cdot y_1,~y_2 / 2)$ \End \End
\li $z \gets y_3$
\end{codebox}

$odd(x)$ истинно тогда и только тогда, когда $x$ нечетно.



% дискретное логарифмирование


%%%\chapter{Поведенческие спецификации}
%%%TBD
%%



%\chapter{Формальные спецификации в различных предметных областях}


%%\chapter{Специфицирование систем реального размера}
%%Спецификация для функции append в <<исполнимой>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value append: L >< L -> L
%%    append(x, y) is x ^ y
%%\end{lstlisting}
%%
%%Спецификация для функции append в <<логической>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value append: L >< L -> L
%%    append(x, y) as z
%%    post
%%        len z = len x + len y /\
%%        (all i: Nat :- i isin inds x => z(i) = x(i)) /\
%%        (all i: Nat :- i isin inds y => z(i+len x) = y(i))
%%\end{lstlisting}
%%
%%Спецификация для функции reverse в <<исполнимой>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value reverse: L -> L
%%    reverse(x) is
%%        local variable y : L :- y = <..> in
%%            for xi in x do
%%                y := <.xi.> ^ y
%%            end;
%%            y;
%%        end
%%\end{lstlisting}
%%
%%Спецификация для функции reverse в <<логической>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value reverse: L -> L
%%  reverse(x) as y
%%  post len x = len y /\
%%    (all i: Nat :- i isin inds x => y(i) = x(len x + 1 - i))
%%\end{lstlisting}
%%
%%Спецификация для функции reverse в <<алгебраической>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value reverse: L -> L
%%axiom
%%    reverse(<..>) is <..>,
%%    all x, y: L :- reverse(x^y) is reverse(y) ^ reverse(x)
%%\end{lstlisting}
%%
%%Что из этого короче? Что понятнее? Что лучше? (зависит от задачи)
%
%% задача - выбрать и правильно смоделировать самое главное в алгоритме:
%% gzip, протокол MESI, map/reduce, mp3, google chrome... (в зависимости от варианта задания--посмотреть,что интересует молодежь на Хабре) -- так, чтобы другой человек мог сам понять и получить это новое знание. В качестве примера, можно рассмотреть то, что я писал в диссертации - поймут студенты?
%% DOM:
%%http://www.w3.org/TR/DOM-Level-3-Core/core.html#ID-184E7107–???DOM Core 3
%%http://ru.wikipedia.org/wiki/Document_Object_Model-

\appendix
\include{rslprior}

\pagebreak
\addcontentsline{toc}{section}{Литература}
\bibliographystyle{gost780s}
\bibliography{rslbooks}

\end{document}
